All pull requests

Pull requests

• feat(RingTheory/Multiplicity): multiplicity_pow without finiteness hypothesis

  WIP
  #45473·xroblot opened Oct 29, 2026Collaborator·

  ·
  1

• feat: use IsApply for OneHom

  large-importt-algebra
  #45472·EtienneC30 opened Oct 29, 2026Member·

  ·
  1

• chore: remove declarations deprecated between 2021-10-29 and 2026-04-29

  #45471·mathlib-nolints[bot] opened Oct 29, 2026Bot·

  ·
  2

• feat(Data): theorem about List.splitBy of List.append when getLast of first list and head of the second list are related

  new-contributort-data
  #45470·benpigchu opened Oct 29, 2026Contributor·

  ·
  2

• feat: linter against defeq abuse in ⟨...⟩ notation

  t-linter
  #45469·JovanGerb opened Oct 29, 2026Contributor·

  ·
  1

• feat: un-revert "feat: enable Verso if no syntax or doc-gen changes (#45031)" (#45094)

  bors-stagingdocumentationready-to-merge
  #45466·Vierkantor opened Oct 29, 2026Contributor·

  ·
  3

• feat(FieldTheory/Finite): sum of the powers of the elements of a finite field

  t-algebra
  #45465·xroblot opened Oct 29, 2026Collaborator·

  ·
  4

• feat(Data/Nat/GCD): a ^ b - 1 ∣ a ^ c - 1 ↔ b ∣ c

  t-data
  #45464·xroblot opened Oct 29, 2026Collaborator·

  ·
  1

• feat(NumberTheory/MulChar): multiplicative characters are local homomorphisms

  t-number-theory
  #45463·xroblot opened Oct 29, 2026Collaborator·

  ·
  1

• feat(Probability/Moments): the Paley–Zygmund inequality

  LLM-generatedt-measure-probability
  #45462·CoolRmal opened Oct 29, 2026Contributor·

  ·
  1

• chore(FieldTheory/KummerPolynomial): rename theorems

  bors-stagingready-to-merget-algebra
  #45461·plp127 opened Oct 29, 2026Contributor·

  ·
  4

• feat(CategoryTheory/Functor): left derived bifunctors

  t-category-theory
  #45460·joelriou opened Oct 29, 2026Contributor·

  ·
  1

• chore: downstream-lean4 adaptations for nightly-2026-10-27

  increases-technical-debtnew-contributor
  #45458·downstream-lean4[bot] opened Oct 29, 2026Bot·

  ·
  2

• feat: the attribute on deprecated linter

  increases-technical-debtt-linter
  #45457·adomani opened Oct 29, 2026Contributor·

  ·
  9

• feat(Algebra/Order/Ring): more constructors for ring (pre)orderings

  increases-technical-debtlarge-importmerge-conflictt-algebra
  #45456·artie2000 opened Oct 29, 2026Collaborator·1 task done·

  ·
  3

• feat(Algebra/Ring/Subsemiring): more properties of pointed, spanning subsemiring

  increases-technical-debtlarge-importmerge-conflictt-algebra
  #45455·artie2000 opened Oct 29, 2026Collaborator·1 task done·

  ·
  3

• feat(Algebra/Group/Submonoid): bot is pointed, top is not

  t-algebra
  #45454·artie2000 opened Oct 29, 2026Collaborator·

  ·
  1

• chore: remove transparency set_options in SimpleGraph, part 2

  LLM-generatedt-combinatoricstech debt
  #45453·Parcly-Taxel opened Oct 29, 2026Collaborator·

  ·
  1

• chore: remove transparency set_options in SimpleGraph, part 1

  t-combinatoricstech debt
  #45451·Parcly-Taxel opened Oct 29, 2026Collaborator·

  ·
  1

• chore(NumberTheory): replace anonymous constructor by .mk in ArithmeticFunction

  t-number-theorytech debt
  #45450·mcdoll opened Oct 29, 2026Member·

  ·
  1

• feat: more lemmas about differentiability of sections

  t-differential-geometry
  #45449·grunweg opened Oct 28, 2026Contributor·

  ·
  1

• feat(Geometry/Manifold/VectorBundle/Basic): small missing API lemmas

  t-differential-geometry
  #45448·grunweg opened Oct 28, 2026Contributor·

  ·
  1

• feat(Analysis/Normed/Lp): interpolate finite matrix bounds

  LLM-generatednew-contributort-analysis
  #45447·janbernloehr opened Oct 28, 2026·

  ·
  2

• feat: converting between sections and dependent functions

  blocked-by-other-PRt-differential-geometryWIP
  #45446·grunweg opened Oct 28, 2026Contributor·2 tasks·

  ·
  2

• feat(Analysis/Normed/Lp): detect PiLp norms by conjugate pairings

  LLM-generatednew-contributort-analysis
  #45445·janbernloehr opened Oct 28, 2026·

  ·
  2