All pull requests

Pull requests

• feat: x ≤ 1 implies x ^ y ≤ 1 on ordinals

  easyt-set-theory
  #45104·vihdzp opened Oct 20, 2026Collaborator·

  ·
  1

• feat(Analysis/Gamma): a convenient ‖Gamma s‖ ≤ ‖Gamma (s + n)‖

  t-analysis
  #45103·wwylele opened Oct 20, 2026Collaborator·

  ·
  1

• chore(Analysis/Calculus/FDeriv/Analytic): tag more @[fun_prop]

  t-analysis
  #45102·wwylele opened Oct 20, 2026Collaborator·

  ·
  1

• chore: use IsApply for CauSeq

  t-algebra
  #45101·mcdoll opened Oct 20, 2026Member·

  ·
  1

• feat: many simp theorems for Ordinal.lift

  t-set-theory
  #45099·vihdzp opened Oct 20, 2026Collaborator·

  ·
  9

• chore: rename Cardinal.mk_Iio_ordinal → Ordinal.cardinalMk_Iio

  t-set-theory
  #45098·vihdzp opened Oct 20, 2026Collaborator·

  ·
  1

• chore: generalize lemmas about measurability of biUnion

  t-measure-probability
  #45097·sgouezel opened Oct 20, 2026Contributor·

  ·
  1

• fix(cache): retry hard download failures in a fresh pass

  CI
  #45096·marcelolynch opened Oct 20, 2026Contributor·

  ·
  1

• feat(CategoryTheory/SmallObject): start a well-order induction from a non-minimal element

  blocked-by-other-PRlarge-import
  #45095·robin-carlier opened Oct 20, 2026Contributor·1 task·

  ·
  2

• feat: use IsApply for ContinuousMap

  blocked-by-other-PRt-topology
  #45093·EtienneC30 opened Oct 20, 2026Member·1 task·

  ·
  2

• refactor(Combinatorics/SimpleGraph): reuse leaf connectivity proof

  LLM-generatednew-contributort-combinatorics
  #45091·Fieldnote-Echo opened Oct 20, 2026Contributor·

  ·
  8

• refactor(Topology/Algebra/OpenSubgroup): drop T1 assumption in tendsto_coe_cofinite_of_isDiscrete

  t-topology
  #45089·justus-springer opened Oct 20, 2026Collaborator·

  ·
  1

• feat: use IsApply for BoundedContinuousFunction

  blocked-by-other-PRt-topology
  #45087·EtienneC30 opened Oct 20, 2026Member·1 task·

  ·
  2

• feat(rm_set_option): scan for options of any value

  CI
  #45085·grunweg opened Oct 20, 2026Contributor·1 task done·

  ·
  13

• perf: lower prio of expensive instance

  t-algebra
  #45083·fpvandoorn opened Oct 20, 2026Member·

  ·
  3

• chore: use IsApply for ZeroAtInfty

  large-import
  #45081·mcdoll opened Oct 20, 2026Member·

  ·
  1

• chore(NumberTheory/Cyclotomic/Gal): remove simp lemmas for autEquivPow

  t-number-theory
  #45078·xroblot opened Oct 20, 2026Collaborator·

  ·
  1

• feat: use IsApply for SimpleFunc

  maintainer-merget-measure-probability
  #45077·EtienneC30 opened Oct 20, 2026Member·

  ·
  7

• feat(Algebra/Lie/SemiDirect): add natural ideal and subalgebra; add equivalences

  new-contributort-algebra
  #45076·vdelbarc opened Oct 20, 2026Contributor·

  ·
  2

• feat(LinearAlgebra): characterize submodules with rank-one quotients

  new-contributort-algebra
  #45075·vdelbarc opened Oct 20, 2026Contributor·

  ·
  2

• refactor(Tactic/Positivity): add a cache

  new-contributort-meta
  #45072·HugLycan opened Oct 20, 2026Contributor·

  ·
  4

• feat(Geometry/Manifold): the Riemann curvature of a covariant derivative

  LLM-generatednew-contributort-differential-geometry
  #45069·korbonits opened Oct 20, 2026Contributor·

  ·
  3

• feat(Tactic/Linter/Header): profile the header linter

  easyt-linter
  #45068·thorimur opened Oct 20, 2026Contributor·

  ·
  3

• feat(AlgebraRepresentation): add symmetric nondegenerate algebra and trace representative

  blocked-by-other-PRt-ring-theoryWIP
  #45067·JX-Mo opened Oct 20, 2026Contributor·2 tasks·

  ·
  7

• chore: remove unnecessary set_option lines

  auto-merge-after-CItech debt
  #45066·mathlib-nolints[bot] opened Oct 20, 2026Bot·1 task done·

  ·
  1