All pull requests

Pull requests

• 🚧 chore: bump mathlib to 300d0e5 — needs help

  #1201·Kevin Buzzard (kbuzzard) opened Oct 3, 2026Collaborator·

  ·
  1

• feat: prove canonicalForm in HurwitzRatHat

  awaiting-review
  #1183·Ty (theTyster) opened Aug 26, 2026·

  ·
  1

• refactor: replace private summation lemmas with Mathlib's API

  #1179·Malhar A. Patel (Mal-Pat) opened Aug 19, 2026Contributor·

  ·

• feat(Data/HurwitzRatHat): prove injectivity of j₁ and j₂ embeddings v…

  #1178·navindutta opened Aug 19, 2026·

  ·

• feat(EllipticCurve/Torsion): prove DistribMulAction instance for Weie…

  #1177·navindutta opened Aug 19, 2026·

  ·

• refactor: replace private ℕ+/ℕ transfer lemmas with mathlib's API

  #1173·Pepa Montero Jimena (pepamontero) opened Aug 14, 2026Contributor·

  ·

• Discharge GL₀ constant-form and elliptic-curve action sorries

  #1155·Fabian Franz (fabianx-ai) opened Aug 6, 2026·

  ·
  1

• feat: prototype native RightModule/Bimodule classes

  WIP
  #1152·Kevin Buzzard (kbuzzard) opened Aug 4, 2026Collaborator·

  ·

• fix: make the pre-push scripts work on a lakefile.toml checkout without leanblueprint

  awaiting-review
  #1134·anagnorisis2peripeteia opened Jul 24, 2026·

  ·
  1

  1

• perf: remove the respectTransparency workarounds in the #889/#891 hotspot files

  awaiting-review
  #1132·anagnorisis2peripeteia opened Jul 23, 2026·

  ·
  1

  1

• Relate QHat to the finite adele ring

  awaiting-review
  #1130·Pedro Paulo Marques do Nascimento (pedromnasc) opened Jul 22, 2026·

  ·
  1

  1

• Convert FLTTest to the module system

  #1129·Pedro Paulo Marques do Nascimento (pedromnasc) opened Jul 22, 2026·

  ·
  1

• feat: prove injective_hRat and injective_zHat in HurwitzRatHat

  awaiting-review
  #1115·Ty (theTyster) opened Jul 11, 2026·

  ·
  4

• Add Voight ramification challenge

  #1114·Jack McCarthy (Deicyde) opened Jul 11, 2026Contributor·

  ·

• refactor: move the exact-couple and spectral-sequence libraries into the Slop namespace

  #1111·Akhil Mathew (j2d9w5xtjn-png) opened Jul 10, 2026Contributor·

  ·

• feat(KnownIn1980s): state Local Duality for finite discrete modules in continuous cohomology

  #1110·Edison Xie (Whysoserioushah) opened Jul 10, 2026Contributor·

  ·
  10

• feat: tateCurve file work

  #1109·William Coram (WilliamCoram) opened Jul 10, 2026Contributor·

  ·
  1

• feat: exact couples and filtered-complex spectral sequences (Slop)

  #1108·Akhil Mathew (j2d9w5xtjn-png) opened Jul 10, 2026Contributor·

  ·

• chore: remove backward.isDefEq.respectTransparency in finite adele/te…

  #1107·maddycrim opened Jul 10, 2026Contributor·

  ·

• feat: add Poitoutate nine term complex, dependent on PR 1110

  #1105·Samanda Z (ZSherrifield) opened Jul 10, 2026·

  ·

• feat(Slop): Henselian pairs

  #1102·Akhil Mathew (j2d9w5xtjn-png) opened Jul 9, 2026Contributor·

  ·

• Add quaternion maximal orders (Voight 15.5.2)

  #1092·Jack McCarthy (Deicyde) opened Jul 8, 2026Contributor·

  ·

• feat: if rho is irred and hardly ramified then rho|G_{Q(zeta_p)} is abs irred

  #1089·Kevin Buzzard (kbuzzard) opened Jul 8, 2026Collaborator·

  ·

• feat(KnownIn1980s): two conjugate characters imply induced from index-two subgroup

  #1084·baimurzzin opened Jul 7, 2026·

  ·

• Ribet lemma for flt repo

  #1083·bryan-hu opened Jul 7, 2026·

  ·