All pull requests

Pull requests

• refactor(Algebra): move from aesop to grind for IsSquare

  t-algebrat-meta
  #45262·artie2000 opened Oct 24, 2026Collaborator·

  ·
  2

• feat: use IsApply for OneHom, MulHom and MonoidHom

  large-importt-algebra
  #45261·EtienneC30 opened Oct 24, 2026Member·

  ·
  1

• feat:(SetTheory/Ordinal/Arithmetic): prove ofNat version of simp lemma

  easyt-set-theory
  #45260·vihdzp opened Oct 24, 2026Collaborator·

  ·
  2

• chore(LinearAlgebra/Countable): remove Finsupp namespace

  t-algebra
  #45259·justus-springer opened Oct 24, 2026Collaborator·

  ·
  1

• refactor: OrderDual as a one-field structure

  LLM-generatedtech debt
  #45258·Parcly-Taxel opened Oct 24, 2026Collaborator·

  ·
  1

• feat(Analysis/Fourier): fourierCoeff extracts coefficients from Fourier series

  t-analysis
  #45257·wwylele opened Oct 24, 2026Collaborator·

  ·
  5

• feat(CategoryTheory/Monad/EquivMon): Upgrade equivalence to isomorphism

  awaiting-authornew-contributort-category-theorytech debtwill-close-soon
  #45256·viliml opened Oct 24, 2026Contributor·

  ·
  4

• refactor(RingTheory/Ideal/Norm/AbsNorm): replace unprimed absNorm lemmas by their primed versions

  t-ring-theoryWIP
  #45255·xroblot opened Oct 24, 2026Collaborator·

  ·
  1

• fix(Tactic/Linarith): linarith? suggestion replaces the whole tactic call

  new-contributort-meta
  #45254·BorisTheBrave opened Oct 24, 2026Contributor·

  ·
  2

• chore(Order/CompleteLattice): use @[to_dual] more

  t-order
  #45253·YaelDillies opened Oct 24, 2026Contributor·

  ·
  1

• feat(Order): ι →₀ α is conditionally complete when α is

  t-order
  #45252·YaelDillies opened Oct 24, 2026Contributor·

  ·
  3

• feat(Order): OrderIso.prodCongr

  t-order
  #45251·YaelDillies opened Oct 24, 2026Contributor·

  ·
  1

• refactor(Order): generalise the CompleteLattice instance on WithTop

  t-order
  #45250·YaelDillies opened Oct 24, 2026Contributor·

  ·
  1

• feat(Order): transfer instances for complete lattices

  t-order
  #45249·YaelDillies opened Oct 24, 2026Contributor·

  ·
  1

• feat(Order): constructor for OrderIso from a bijective order-preserving map

  t-order
  #45248·YaelDillies opened Oct 24, 2026Contributor·

  ·
  1

• chore(Algebra/Order): split out the order on Associates

  t-algebrat-order
  #45247·YaelDillies opened Oct 24, 2026Contributor·

  ·
  1

• feat(Algebra): characterise divisibility in WithZero

  t-algebra
  #45246·YaelDillies opened Oct 24, 2026Contributor·

  ·
  1

• feat(Algebra): right-divisibility under a hom

  t-algebra
  #45245·YaelDillies opened Oct 24, 2026Contributor·

  ·
  1

• chore(Order): generalise OrderIso.withTopCongr to preorders

  easymaintainer-merget-order
  #45244·YaelDillies opened Oct 24, 2026Contributor·

  ·
  3

• doc(Topology/Order/LocalExtr): fix typos and outdated references

  documentationt-ordert-topology
  #45243·SnirBroshi opened Oct 24, 2026Collaborator·

  ·
  1

• chore(LinearAlgebra/Matrix/SpecialLinearGroup): add missing api

  t-algebra
  #45242·Nicola9Falciola opened Oct 24, 2026Contributor·

  ·
  1

• refactor(Algebra/RestrictScalars): change the definition of RestrictScalars

  t-algebratech debtWIP
  #45240·jjdishere opened Oct 24, 2026Collaborator·

  ·
  2

• feat(Probability): define the leastGT stopping time

  browniant-measure-probability
  #45239·RemyDegenne opened Oct 24, 2026Contributor·

  ·
  1

• feat: describe members of countableSupClosure with monotone sequences

  brownianLLM-generatedt-measure-probabilityt-order
  #45238·RemyDegenne opened Oct 24, 2026Contributor·

  ·
  1

• feat(Probability): define complete filtrations

  browniant-measure-probability
  #45237·RemyDegenne opened Oct 24, 2026Contributor·

  ·
  1