All pull requests

Pull requests

• refactor(RingTheory/FractionalIdeal): make spanSingleton a monoid with zero homomorphism

  t-ring-theory
  #44475·xroblot opened Oct 4, 2026Collaborator·

  ·
  1

• refactor(SpecificGroups/Cyclic/Basic): split out heavy-import file

  t-group-theory
  #44473·vlad902 opened Oct 4, 2026Collaborator·

  ·
  2

• feat(Combinatorics/SImpleGraph/Paths): s(u, w) ∈ p.edges ↔ w = p.snd for paths

  t-combinatorics
  #44472·SnirBroshi opened Oct 4, 2026Collaborator·

  ·
  1

• feat(Algebra/Ring/Parity): add two_pow_ne_three_pow and Nat parity lemmas

  LLM-generatednew-contributort-algebra
  #44471·NachoPeinador opened Oct 4, 2026·

  ·
  10

• feat(SetTheory/Ordinal/Exponential): opow_le_of_isSuccLimit works for c ≠ 0

  t-set-theory
  #44470·SnirBroshi opened Oct 4, 2026Collaborator·

  ·
  3

• refactor(Tactic/Linarith): use Lean polynomial arithmetic

  t-meta
  #44469·kim-em opened Oct 4, 2026Contributor·

  ·
  3

• fix(Wanted/Probability): delete the false condVar_of_hasLaw_binomial

  LLM-generatednew-contributort-measure-probability
  #44467·vincentqb opened Oct 3, 2026·

  ·
  4

• refactor: replace bundled commutative classes by IsMulCommutative (experiment)

  LLM-generatedmerge-conflict
  #44466·Deicyde opened Oct 3, 2026Contributor·

  ·
  3

• fix: handle nested conditionals in to_dual

  new-contributort-meta
  #44465·ishanrk opened Oct 3, 2026·

  ·
  1

  2

• feat(AlgebraicTopology/SimplicialSet): the subdivision functor preserves anodyne extensions

  t-algebraic-topologytech debtWIP
  #44464·joelriou opened Oct 3, 2026Contributor·

  ·
  1

• fix(Order/Fin): fix the type of toEmbedding lemma

  t-order
  #44463·wwylele opened Oct 3, 2026Collaborator·

  ·
  11

• feat(Geometry/Euclidean): the corner simplex

  blocked-by-other-PRlarge-import
  #44462·wwylele opened Oct 3, 2026Collaborator·2 tasks·

  ·
  2

• doc: fix mismatched parentheses in docstrings

  awaiting-authorLLM-generated
  #44457·emlis42 opened Oct 3, 2026Contributor·

  ·
  7

• chore(GroupTheory/Sylow): fix Sylow field names

  maintainer-merget-group-theory
  #44454·SnirBroshi opened Oct 3, 2026Collaborator·

  ·
  3

• chore(Combinatorics/Additive/Corner): use explicit Fin embeddings and kill TODOs

  maintainer-merget-combinatoricstech debt
  #44453·yuanyi-350 opened Oct 3, 2026Collaborator·

  ·
  4

• chore(GroupTheory/Finiteness): golf Submonoid.fg_of_divisive

  t-group-theory
  #44450·SnirBroshi opened Oct 3, 2026Collaborator·

  ·
  3

• feat(Data/Nat/Choose/Bounds): an upper-bound for functions with Ramse…

  t-data
  #44448·thefundamentaltheor3m opened Oct 3, 2026Collaborator·

  ·
  6

• chore(Algebra/Tropical): make instance diamond linter happy

  t-algebra
  #44447·JovanGerb opened Oct 3, 2026Contributor·

  ·
  1

• chore: adaptation for upcoming on_goal change

  t-meta
  #44446·JovanGerb opened Oct 2, 2026Contributor·

  ·
  1

• perf(TacticAnalysis): reimplement findTacticSeqs

  t-meta
  #44445·JovanGerb opened Oct 2, 2026Contributor·

  ·
  4

• feat(Topology/Algebra/IsUniformGroup): more versions of isUniformGroup_of_commGroup

  blocked-by-other-PRt-group-theoryt-topology
  #44444·plp127 opened Oct 2, 2026Contributor·1 task·

  ·
  2

• feat(Topology/Algebra/IsUniformGroup): group is left/right uniform group iff it's equal to left/right uniformity

  blocked-by-other-PRt-group-theoryt-topology
  #44443·plp127 opened Oct 2, 2026Contributor·1 task·

  ·
  2

• feat(LinearAlgebra/LinearIndependent/Basic): scaling by right-regular elements preserves linear independence

  new-contributort-algebra
  #44442·aebrose opened Oct 2, 2026Contributor·

  ·
  2

• feat(Computability/TuringMachine): prove TM2ComputableInPolyTime.comp (proof_wanted)

  blocked-by-other-PRfile-removedLLM-generatednew-contributort-computability
  #44441·vincentqb opened Oct 2, 2026·1 task·

  ·
  4

• feat(Computability/TuringMachine): bound the output length of a TM2 run

  LLM-generatednew-contributort-computability
  #44440·vincentqb opened Oct 2, 2026·

  ·
  3