All pull requests

Pull requests

• perf(FlexibleLinter): early exit

  t-linter
  #44461·JovanGerb opened Oct 3, 2026Contributor·

  ·
  3

• feat(RingTheory/Algebraic/Basic): add non-algebraic multiplication transference theorems

  new-contributort-ring-theory
  #44460·NachoPeinador opened Oct 3, 2026·

  ·
  5

• chore: testing

  increases-technical-debtWIP
  #44459·xroblot opened Oct 3, 2026Collaborator·

  ·
  4

• feat(SetTheory/Ordinal): add characterization of exponentially principal ordinals

  new-contributort-set-theory
  #44458·franv314 opened Oct 3, 2026Contributor·

  ·
  2

• doc: fix mismatched parentheses in docstrings

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

  ·
  5

• 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/Sylow): golf Sylow.directProductOfNormal

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

  ·
  8

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

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

  ·
  1

• 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

• test: linter performance

  t-linter
  #44439·JovanGerb opened Oct 2, 2026Contributor·

  ·
  15

• perf(Linter/OldObtain): reimplement by overriding the obtain syntax

  t-linter
  #44438·JovanGerb opened Oct 2, 2026Contributor·

  ·
  5

• perf(Analysis/Normed/Lp/SmoothApprox): manifold-free proof of smooth approximation in Lp

  new-contributort-analysis
  #44437·FawadHa1der opened Oct 2, 2026Contributor·

  ·
  3

• perf(Linter): bundle instance linters into one linter

  #44436·JovanGerb opened Oct 2, 2026Contributor·

  ·
  3

• chore(LinearAlgebra/Span/Basic): add a couple of missing lemmas for toSpanSingleton

  easyt-algebra
  #44435·themathqueen opened Oct 2, 2026Member·

  ·
  1

• chore(RingTheory/IntegralClosure): remove redundant local instances in proofs

  maintainer-mergenew-contributort-ring-theory
  #44434·sun123zxy opened Oct 2, 2026Contributor·

  ·
  6

• feat(Tactic/NormCharpoly): add the norm_charpoly simproc and the eval_charpoly tactic

  blocked-by-other-PR
  #44433·paulcadman opened Oct 2, 2026Contributor·4 tasks·

  ·
  2