All pull requests

Pull requests

• chore: remove redundant theorem hypotheses across Mathlib

  LLM-generated
  #45525·kim-em opened Oct 31, 2026Contributor·

  ·
  3

• feat(Tactic): add opt-in droppable hypothesis linter

  LLM-generatedt-linter
  #45523·kim-em opened Oct 31, 2026Contributor·

  ·
  1

• feat: add the Grigorchuk group

  blocked-by-other-PRnew-contributort-geometric-group-theory
  #45522·EzequielS2 opened Oct 31, 2026Contributor·1 task·

  ·
  3

• feat: add automorphisms of the infinite binary tree

  new-contributort-geometric-group-theory
  #45521·EzequielS2 opened Oct 31, 2026Contributor·

  ·
  2

• feat: add growth of finitely generated groups

  new-contributort-geometric-group-theory
  #45520·EzequielS2 opened Oct 31, 2026Contributor·

  ·
  2

• chore(LinearAlgebra/Matrix): add api for compatibility between reindex and map for GL and Matrix

  t-algebra
  #45519·Nicola9Falciola opened Oct 30, 2026Contributor·

  ·
  2

• feat(Logic/Equiv/Fin/Basic): extension/deletion operations on permutations on Fin n

  new-contributort-logic
  #45514·PSchwahn opened Oct 30, 2026Contributor·

  ·
  3

• feat(Data/Fin/Tuple): add Fin.cons_cons_swap

  new-contributort-data
  #45513·PSchwahn opened Oct 30, 2026Contributor·

  ·
  2

• feat: add various lemmas about cyclotomic extensions

  #45512·riccardobrasca opened Oct 30, 2026Member·

  ·
  1

• feat(Data/Subtype): simp lemma for Subtype.val composed with Subtype.map

  easyt-data
  #45511·SnirBroshi opened Oct 30, 2026Collaborator·

  ·
  1

• chore(Testing): lower the priority of Module.Flat.isTorsionFree

  t-ring-theory
  #45510·xroblot opened Oct 30, 2026Collaborator·

  ·
  3

• feat(RingTheory/ZMod/UnitsCyclic): (ZMod (2 ^ (n + 2)))ˣ is ±1 times the powers of 5

  WIP
  #45509·xroblot opened Oct 30, 2026Collaborator·

  ·
  2

• refactor: make InfinitePlace.Completion an abbrev

  #45508·smmercuri opened Oct 30, 2026Collaborator·

  ·
  3

• ci: validate dependency pins in lake-manifest.json

  CI
  #45507·marcelolynch opened Oct 30, 2026Contributor·

  ·
  1

• chore: fix namespace in a deprecation

  documentationt-measure-probability
  #45506·EtienneC30 opened Oct 30, 2026Member·

  ·
  1

• feat(GroupTheory/Abelianization/Defs): additivize Abelianization

  awaiting-authornew-contributort-group-theory
  #45505·osmangroup opened Oct 30, 2026Contributor·

  ·
  6

• feat: use IsApply for Function.Embedding

  blocked-by-other-PRt-data
  #45504·EtienneC30 opened Oct 30, 2026Member·1 task·

  ·
  2

• chore(Algebra/Order/Ring): golf proof about geometric sum

  easyt-algebra
  #45503·artie2000 opened Oct 30, 2026Collaborator·

  ·
  3

• chore(Algebra/Polynomial): golf normalize lemmas

  easyt-algebra
  #45502·artie2000 opened Oct 30, 2026Collaborator·

  ·
  2

• chore: lemmas about NNReal.mk

  awaiting-authort-datat-order
  #45501·eric-wieser opened Oct 30, 2026Member·

  ·
  3

  

• feat(Data/Set/Finite): add directed union and intersection lemmas

  t-data
  #45500·Jun2M opened Oct 30, 2026Collaborator·

  ·
  2

• feat(RingTheory/Unramified/Finite): add equalizerIdempotent

  awaiting-authorLLM-generatedt-algebrat-ring-theory
  #45499·tb65536 opened Oct 29, 2026Contributor·

  ·
  10

  

• feat(LinearAlgebra): identify Sp₂(R) with SL₂(R)

  LLM-generatednew-contributort-algebra
  #45498·ShirinShafaie opened Oct 29, 2026·1 task done·

  ·
  3

• feat(MeasureTheory): tightness in separable Hilbert spaces

  LLM-generatednew-contributort-measure-probability
  #45497·chenle02 opened Oct 29, 2026·

  ·
  2

• feat(MeasureTheory): the Lyapunov's convexity theorem

  t-measure-probability
  #45496·lua-vr opened Oct 29, 2026Contributor·

  ·
  2