All pull requests

Pull requests

• feat(LinearAlgebra/Matrix/Determinant/Basic): the Cauchy–Binet formula for 2 × 2 minors

  new-contributort-algebra
  #44757·mycaule opened Oct 11, 2026·

  ·
  2

• feat(Algebra/Polynomial/RingDivision): polynomials coprime to X - C a

  new-contributort-algebra
  #44756·mycaule opened Oct 11, 2026·

  ·
  2

• feat(Algebra/CharP/HasseDeriv): the Hasse derivatives are linear over X ^ (p ^ e)

  blocked-by-other-PRnew-contributort-algebra
  #44755·mycaule opened Oct 11, 2026·1 task·

  ·
  3

• feat(Analysis/Complex): existence of analytic logs and roots

  t-analysis
  #44754·ajirving opened Oct 11, 2026Contributor·

  ·
  2

• chore(RingTheory/IntegralClosure/IsIntegralClosure): omit instance name

  easyt-ring-theory
  #44753·SnirBroshi opened Oct 11, 2026Collaborator·

  ·
  1

• feat(Algebra/CharP/Two): add basic lemmas

  t-algebra
  #44751·mortarsanjaya opened Oct 11, 2026Contributor·

  ·
  1

• feat(Analysis/SpecialFunctions/Gaussian): integrability of (1 + |x|)^k * exp (-b x^2 + a |x|)

  new-contributort-analysis
  #44750·DrMurphyIsIn opened Oct 11, 2026·

  ·
  2

• feat(NumberTheory/LSeries): Bohr almost periodicity of Dirichlet series

  new-contributort-number-theory
  #44749·DrMurphyIsIn opened Oct 11, 2026·

  ·
  3

• feat(Analysis/SpecialFunctions/Exponential): ‖exp x - 1‖ ≤ ‖x‖ * exp ‖x‖

  new-contributort-analysis
  #44748·DrMurphyIsIn opened Oct 11, 2026·

  ·
  2

• feat(Analysis/SpecialFunctions/Gamma): norm of the complex Gamma function is bounded by the real Gamma function

  new-contributort-analysis
  #44747·DrMurphyIsIn opened Oct 11, 2026·

  ·
  2

• feat(Analysis/SpecialFunctions/Gamma): Stirling's formula for the complex Gamma function with remainder

  new-contributort-analysis
  #44746·DrMurphyIsIn opened Oct 11, 2026·

  ·
  3

• doc(SetTheory/Cardinality/Cofinality/Club): improve documentation

  documentationeasyt-set-theory
  #44745·vihdzp opened Oct 11, 2026Collaborator·

  ·
  1

• chore(Algebra/MvPolynomial/Division): change local notation %ᵐᵒⁿᵒᵐⁱᵃˡ → %ᵐ

  easyt-algebra
  #44744·vihdzp opened Oct 11, 2026Collaborator·

  ·
  1

• refactor(Wiedijk100Theorems/AreaOfACircle): deprecate file

  t-measure-probability
  #44743·vihdzp opened Oct 11, 2026Collaborator·

  ·
  1

• feat: weaken even more assumptions on theorems about FloorRing

  help-wantedt-algebra
  #44741·mortarsanjaya opened Oct 11, 2026Contributor·

  ·
  2

• chore(Algebra/Ring/CompTypeclasses): fix a typo and reformat slightly

  new-contributort-algebra
  #44740·user202729 opened Oct 11, 2026Contributor·

  ·
  4

• chore: fix {a a : α} → {a : α}

  easy
  #44739·vihdzp opened Oct 11, 2026Collaborator·

  ·
  1

• feat(Analysis/Normed/Module): generalize currying to seminormed spaces

  t-analysis
  #44738·harahu opened Oct 11, 2026Contributor·

  ·
  1

• feat(Linter): terminal cdot linter using tacticAnalysis

  t-linter
  #44737·JovanGerb opened Oct 11, 2026Contributor·

  ·
  1

• feat(Algebra/CharP/HasseDeriv): vanishing of Hasse derivatives in prime characteristic

  new-contributort-algebra
  #44736·mycaule opened Oct 11, 2026·

  ·
  3

• feat(Data/Nat/Choose/Lucas): p ^ e ∣ n iff p divides n.choose k for 0 < k < p ^ e

  new-contributort-data
  #44735·mycaule opened Oct 11, 2026·

  ·
  2

• feat(RingTheory/LocalProperties/Semilocal): semilocal rings have stable range one

  new-contributort-ring-theory
  #44734·mycaule opened Oct 11, 2026·

  ·
  2

• chore(Tactic/Linter/TextBased): remove the trailing whitespace linter

  t-linter
  #44733·SnirBroshi opened Oct 11, 2026Collaborator·

  ·
  1

• feat(AlgebraicTopology/Reedy/SemiSimplexCategory): the semi-simplex category is direct

  blocked-by-other-PRnew-contributort-algebraic-topology
  #44732·mycaule opened Oct 11, 2026·1 task·

  ·
  4

• feat(AlgebraicTopology/Reedy/Direct): direct categories via well-foundedness

  new-contributort-algebraic-topology
  #44731·mycaule opened Oct 11, 2026·

  ·
  3