feat(Topology/Compactness/CompactSystem): introduce compact Systems#25899

Closed

pfaffelh wants to merge 4477 commits intoleanprover-community:masterfrom

pfaffelh:pfaffelh_compactSystem

This pull request is big! We're only showing the most recent 250 commits

Commits on Jan 9, 2026

feat(CategoryTheory/Sites): relation between `IsPrestack` and the full faithfulness of `toDescentData` (#33179)

joelriou
authored and
pfaffelh
committed
feat: cardinality of Hahn series inverse (#32643)

authored and
pfaffelh
committed
feat: `stdPart x = sSup {r | r < x}` (#33007)

vihdzp
authored and
pfaffelh
committed
feat(Combinatorics/SimpleGraph/Acyclic): characterise maximal acyclic subgraphs (#32043)

authored and
pfaffelh
committed
chore(Topology/Algebra/Module/LinearMap): deprecate duplicate lemmas (#33341)

themathqueen
authored and
pfaffelh
committed
chore(Order/Defs/Unbundled): deprecate `IsSymm` in favor of core's `Std.Symm` (#33325)

SnirBroshi
authored and
pfaffelh
committed
feat(CategoryTheory): Exponentiable morphisms (#31332)

authored and
pfaffelh
committed
chore(Algebra/Central/End): generalize `Algebra.IsCentral.instEnd` (#33301)

themathqueen
authored and
pfaffelh
committed
feat(Homotopy/Lifting): add a lemma about `IsCoveringMapOn` (#33422)

urkud
authored and
pfaffelh
committed
feat(Probability): Right continuous filtrations (#33371)

kex-y
authored and
pfaffelh
committed
feat: FTaylorSeries of the composition with an affine map (#33459)

sgouezel
authored and
pfaffelh
committed
chore: Fix Dihedral comments (#33483)

ldct
authored and
pfaffelh
committed
feat(CategoryTheory/Sites): stacks (#33195)

joelriou
authored and
pfaffelh
committed
feat(RingTheory): polynomial is integral <-> coeffs are integral (#33468)

erdOne
authored and
pfaffelh
committed
feat(Algebra/GroupWithZero/NonZeroDivisors): add some lemmas about multiplication (#32773)

Hagb
authored and
pfaffelh
committed
feat: simp lemmas PrimeSpectrum.asIdeal_bot/top (#33489)

xgenereux
authored and
pfaffelh
committed
feat: `IsStrictOrderedRing (Lex R⟦Γ⟧)` (#33398)

vihdzp
authored and
pfaffelh
committed
feat(RingTheory/RootsOfUnity/PrimitiveRoots): add primitiveRootsPowEquivOfCoprime (#26483)

metakunt
authored and
pfaffelh
committed
doc(translate): improve discoverability of trace options (#33500)

JovanGerb
authored and
pfaffelh
committed
feat(Algebra/Order/SuccPred): simplify n+1 ≤ ... and ... < n+1 (#33320)

vihdzp
authored and
pfaffelh
committed
feat: subfield of Hahn series bounded by a cardinal (#32648)

authored and
pfaffelh
committed
feat(Algebra/Group/Action): add `smul_set_eq_univ` (#33515)

urkud
authored and
pfaffelh
committed
chore(Algebra/MonoidAlgebra/Basic): rename variables (#33516)

YaelDillies
authored and
pfaffelh
committed
feat: file for lemmas about MvPolynomials over NoZeroDivisors (#25925)

BoltonBailey
authored and
pfaffelh
committed
feat(MetricSpace): add `eventually_ball_subset` (#33512)

urkud
authored and
pfaffelh
committed
feat(ToIntervalMod): add missing lemmas (#33442)

urkud
authored and
pfaffelh
committed
feat(MetricSpace/Algebra): prove uniform continuity of `(· • ·)` (#33517)

urkud
authored and
pfaffelh
committed
refactor: rename `≤ᵥ` to `vle` and `<ᵥ` to `vlt` (#33040)

vihdzp
authored and
pfaffelh
committed
ci: add tracing option to linting steps (#33474)

bryangingechen
authored and
pfaffelh
committed
feat(RingTheory/TensorProduct/MonoidAlgebra): additivise (#33482)

YaelDillies
authored and
pfaffelh
committed
feat(Schwarz): generalize domain (#33511)

urkud
authored and
pfaffelh
committed
chore(Data/Finsupp): rename `finsuppProdEquiv` to `curryEquiv` (#33521)

YaelDillies
authored and
pfaffelh
committed
feat(CauchyIntegral): add a version of the Cauchy integral theorem (#33509)

urkud
authored and
pfaffelh
committed
feat(CircleIntegral): integral of a finite sum of functions (#33513)

urkud
authored and
pfaffelh
committed
feat(RingTheory/Nilpotent/Exp): add isNilpotent_exp_sub_one (#33473)

anivegesana
authored and
pfaffelh
committed
feat(RingTheory/DedekindDomain/AdicValuation): introduce `intAdicAbv` (#33324)

fbarroero
authored and
pfaffelh
committed
feat(Algebra): characterise when a submodule constructor is equal to `⊥` (#32836)

YaelDillies
authored and
pfaffelh
committed
chore: update Mathlib dependencies 2026-01-03 (#33528)

authored and
pfaffelh
committed
feat(Data/Matrix/Cartan): determinants and simply-laced properties (#33115)

JohnnyTeutonic
authored and
pfaffelh
committed
chore: update Mathlib dependencies 2026-01-04 (#33534)

authored and
pfaffelh
committed
doc(Algebra): fix file refs (#33446)

harahu
authored and
pfaffelh
committed
feat(RingTheory/MvPowerSeries): (mv) PowerSeries version of `expand_char` (#33091)

WenrongZou
authored and
pfaffelh
committed
doc(RingTheory): fix file refs (#33284)

harahu
authored and
pfaffelh
committed
feat(RingTheory/Nakayama): refine Nakayama's lemma 00DV (8) (#33361)

sun123zxy
authored and
pfaffelh
committed
feat(Valuation/Basic): adjust Valuation.IsNontrivial lemmas for fields (#33488)

xgenereux
authored and
pfaffelh
committed
feat(AlgebraicTopology): finite simplicial sets are `ℵ₀`-presentable (#32266)

joelriou
authored and
pfaffelh
committed
refactor(SetTheory/Ordinal/Arithmetic): deprecate `boundedLimitRecOn` (#33319)

vihdzp
authored and
pfaffelh
committed
feat(Geometry/Euclidean/Angle/Oriented/Affine): Add oangle sign lemmas for two intersecting lines (#33365)

zcyemi
authored and
pfaffelh
committed
feat(BigOperators/Finprod): add `finsum_cond_pos` (#33508)

urkud
authored and
pfaffelh
committed
feat(RingTheory/DedekindDomain/GaussLemma): Gauss's Lemma for Dedekind Domains (#33326)

fbarroero
authored and
pfaffelh
committed
fix(CI): prevent empty grep pattern from matching all lean-pr-testing branches (#33546)

kim-em
authored and
pfaffelh
committed
feat: generalise `Ideal.absNorm_eq_pow_inertiaDeg` (#33484)

smmercuri
authored and
pfaffelh
committed
refactor(Algebra/Polynomial/Factors): Deprecate file (#32946)

tb65536
authored and
pfaffelh
committed
feat: Simple lemmas about convergence in WithTop (#33374)

kex-y
authored and
pfaffelh
committed
doc(README): linter -> linters (#33533)

Rida-Hamadani
authored and
pfaffelh
committed
feat(Polynomial/Chebyshev): calculate values of T and U at zero (#33311)

YuvalFilmus
authored and
pfaffelh
committed
feat(Topology/Algebra/Module/Equiv): add 2 lemmas (#33510)

urkud
authored and
pfaffelh
committed
feat(RingTheory): no extension is algebraic over the zero ring (#33540)

YaelDillies
authored and
pfaffelh
committed
feat: lemmas about `Matrix.single` and `diagonal` and `submatrix` (#33547)

eric-wieser
authored and
pfaffelh
committed
feat(CategoryTheory): `FinCategory` instance on `Pairwise` (#33537)

erdOne
authored and
pfaffelh
committed
chore(Analysis/Calculus): remove unnecessary @[expose] from public sections (#33565)

kim-em
authored and
pfaffelh
committed
chore: update Mathlib dependencies 2026-01-05 (#33566)

authored and
pfaffelh
committed
chore(Analysis/SpecialFunctions): remove unnecessary @[expose] from public sections (#33567)

kim-em
authored and
pfaffelh
committed
chore(Analysis/Normed): remove unnecessary @[expose] from public sections (#33568)

kim-em
authored and
pfaffelh
committed
chore(Analysis/Complex): remove unnecessary @[expose] from public sections (#33569)

kim-em
authored and
pfaffelh
committed
chore(Data): remove unnecessary @[expose] from public sections (#33574)

kim-em
authored and
pfaffelh
committed
feat(SimpleGraph): define and prove basic theory of vertex covers (#30129)

vlad902
authored and
pfaffelh
committed
perf(to_fun): remove `ofNat(n)` in `Pi.ofNat_def` (#32940)

JovanGerb
authored and
pfaffelh
committed
chore: golf proofs (#33541)

euprunin
authored and
pfaffelh
committed
chore: golf proofs (#33559)

euprunin
authored and
pfaffelh
committed
chore: mark `Ordinal.enumOrd` with `no_expose` (#33298)

vihdzp
authored and
pfaffelh
committed
ci: run check-lean4checker on self-hosted runner (#33424)

bryangingechen
authored and
pfaffelh
committed
feat: range of `Finsupp` is finite (#33530)

vihdzp
authored and
pfaffelh
committed
chore(Algebra/Order): remove unnecessary @[expose] from public sections (#33570)

kim-em
authored and
pfaffelh
committed
chore(Algebra/Group): remove unnecessary @[expose] from public sections (#33571)

kim-em
authored and
pfaffelh
committed
chore(Algebra): remove unnecessary @[expose] from public sections (#33572)

kim-em
authored and
pfaffelh
committed
chore(RingTheory): remove unnecessary @[expose] from public sections (#33573)

kim-em
authored and
pfaffelh
committed
chore(Topology): remove unnecessary @[expose] from public sections (#33575)

kim-em
authored and
pfaffelh
committed
chore(MeasureTheory): remove unnecessary @[expose] from public sections (#33576)

kim-em
authored and
pfaffelh
committed
chore(CategoryTheory): remove unnecessary @[expose] from public sections (#33577)

kim-em
authored and
pfaffelh
committed
chore(NumberTheory): remove unnecessary @[expose] from public sections (#33578)

kim-em
authored and
pfaffelh
committed
chore(LinearAlgebra,Order): remove unnecessary @[expose] from public sections (#33579)

kim-em
authored and
pfaffelh
committed
chore(Probability,Geometry): remove unnecessary @[expose] from public sections (#33580)

kim-em
authored and
pfaffelh
committed
chore: remove unnecessary @[expose] from public sections (#33581)

kim-em
authored and
pfaffelh
committed
feat(Homology): map between `Ext` induced by exact functor (#31707)

authored and
pfaffelh
committed
feat(RepresentationTheory/Homological/GroupCohomology/Hilbert90): add Hilbert 90 for cyclic groups (#33124)

authored and
pfaffelh
committed
chore(Algebra): move `LinearMap.mul{Left, Right, LeftRight}` to earlier file (#33405)

themathqueen
authored and
pfaffelh
committed
ci: revert changes to wrapper script in #33474 (#33598)

bryangingechen
authored and
pfaffelh
committed
doc(1000.yaml): Add decls of Prokhorov's theorem, Parseval's theorem (#33455)

yuanyi-350
authored and
pfaffelh
committed
chore(Order/Defs/Unbundled): deprecate `IsAsymm` in favor of core's `Std.Asymm` (#33503)

SnirBroshi
authored and
pfaffelh
committed
chore: golf proofs (#33550)

euprunin
authored and
pfaffelh
committed
chore: promote `Matrix.det` from an `abbrev` into a `def` (#33590)

ocfnash
authored and
pfaffelh
committed
feat(MeasureTheory/Integral): add versions of `exists_eq_interval_average` and first mean value theorem for integrals (#30344)

Deep0Thinking
authored and
pfaffelh
committed
feat(CategoryTheory): LCCC sections (constructing right adjoint to `Over.ChosenPullback.pullback`) (#30373)

authored and
pfaffelh
committed
feat(Data/Matrix/Basis): add some lemmas (#31637)

authored and
pfaffelh
committed
feat(NumberTheory/Height/Basic): first installment of heights (#33054)

MichaelStollBayreuth
authored and
pfaffelh
committed
chore: fix some `privateInPublic` proofs (#33591)

JovanGerb
authored and
pfaffelh
committed
feat(Geometry/Euclidean/Angle/Unoriented/Affine): Add Theorem about Sbtw.angle_eq and Wbtw.angle_eq (#33383)

authored and
pfaffelh
committed
feat(LinearAlgebra/Prod): add `range_prodMap` (#33585)

urkud
authored and
pfaffelh
committed
chore(positivity): make tactic lemmas public (#33593)

JovanGerb
authored and
pfaffelh
committed
feat: define `Metric.Snowflaking` (#33114)

urkud
authored and
pfaffelh
committed
feat(Analysis/Complex): exp is covering map (#33564)

alreadydone
authored and
pfaffelh
committed
feat(Analysis/SpecialFunctions/Integrals): add `∫ x : ℝ in a..b, (c ^ 2 + x ^ 2)⁻¹` (#33289)

michelsol
authored and
pfaffelh
committed
feat(Cache): environment-configurable URLs (#33605)

tydeu
authored and
pfaffelh
committed
ci: do not wrap linting step with log parsing script (#33646)

bryangingechen
authored and
pfaffelh
committed
ci: add nanoda verification to daily workflow (#33648)

kim-em
authored and
pfaffelh
committed
fix(Cache): print ProofWidgets build stdout on error (#33651)

authored and
pfaffelh
committed
chore(Data/Option): deprecate `Option.iget` (#33583)

kim-em
authored and
pfaffelh
committed
chore: golf using `grind` (#33074)

euprunin
authored and
pfaffelh
committed
feat(RingTheory): construct etale neighborhood that isolates point in fiber (#32823)

erdOne
authored and
pfaffelh
committed
chore(Topology/Order): generalize `IsCountablyGenerated atTop` instance to `SeparableSpace` (#33486)

gasparattila
authored and
pfaffelh
committed
feat(MeasureTheory/Group/Action): weaken MeasurableSMul to MeasurableConstSMul (#33659)

loefflerd
authored and
pfaffelh
committed
chore: golf proofs (#33616)

authored and
pfaffelh
committed
feat(Data/Nat/Digits): prove the bijection induced by `Nat.ofDigits` and use it to compute the sum of the sum of digits (#31579)

xroblot
authored and
pfaffelh
committed
chore(Data): golf proofs (#33480)

euprunin
authored and
pfaffelh
committed
chore: golf proofs (#33549)

euprunin
authored and
pfaffelh
committed
chore: golf proofs (#33596)

euprunin
authored and
pfaffelh
committed
chore: golf proofs (#33600)

euprunin
authored and
pfaffelh
committed
feat(RingTheory): base change of ideal with flat quotients (#32806)

erdOne
authored and
pfaffelh
committed
feat(Algebra): leading coeff of sum of polynomials with same degree is sum of leading coeffs (#33433)

michelsol
authored and
pfaffelh
committed
feat(Analysis/Normed/Group/Seminorm): define SupSet instances (#32841)

0xTerencePrime
authored and
pfaffelh
committed
chore(RingTheory/MvPowerSeries/Order): deprecate duplicate theorem (#33660)

vihdzp
authored and
pfaffelh
committed
feat: add simp lemma `nhdsSet_eq_bot_iff` (#33623)

j-loreaux
authored and
pfaffelh
committed
feat: add `forall_is{Open,Closed}_iff` (#33624)

j-loreaux
authored and
pfaffelh
committed
feat: filter bases for `nhdsSet` of a compact set in locally compact (regular) spaces (#33625)

j-loreaux
authored and
pfaffelh
committed
fix: `zsmul` lemmas that were about `nsmul` instead (#33652)

vihdzp
authored and
pfaffelh
committed
feat(AlgebraicGeometry/EllipticCurve/Projective): remove unnecessary assumptions in `WeierstrassCurve.Projective.toAffine_slope_of_eq` (#33655)

euprunin
authored and
pfaffelh
committed
refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` (#30706)

authored and
pfaffelh
committed
feat(Polynomial/Derivative): iterated derivative of product of linear factors (#33161)

authored and
pfaffelh
committed
fix(Tactic/WLOG): handle unused let variables (#33632)

plp127
authored and
pfaffelh
committed
feat(Topology): sandwich lemmas for profinite sets (#32660)

authored and
pfaffelh
committed
refactor(EMetricSpace): rename `EMetric.diam` -> `Metric.ediam` (#33558)

urkud
authored and
pfaffelh
committed
chore(Cache): add README and rename USE_FRO_CACHE to MATHLIB_CACHE_USE_CLOUDFLARE (#33647)

kim-em
authored and
pfaffelh
committed
feat(Analysis/Analytic): analytic order of a composition (#33000)

loefflerd
authored and
pfaffelh
committed
feat(LinearAlgebra/AffineSpace/Simplex/Centroid): define centroid and medians (#28411)

zcyemi
authored and
pfaffelh
committed
feat: use new predicate `Meromorphic` in Value Distribution Theory (#33231)

kebekus
authored and
pfaffelh
committed
feat(Analysis/InnerProductSpace): define rank-one operators (#33439)

authored and
pfaffelh
committed
chore(Algebra): some cleanup (#33602)

themathqueen
authored and
pfaffelh
committed
feat(ValuationSubring): toSubring_top (#33610)

xgenereux
authored and
pfaffelh
committed
feat(Algebra/Algebra/Equiv): `f.conj (mulLeft R x) = mulLeft R (f x)` (#33615)

themathqueen
authored and
pfaffelh
committed
fix(Finprod): fix a `to_additive` name (#33638)

urkud
authored and
pfaffelh
committed
feat(Analysis/Fourier): Fourier transform of the convolution (#32992)

mcdoll
authored and
pfaffelh
committed
chore: golf using `grind` and `simp` (#33290)

euprunin
authored and
pfaffelh
committed
feat(Topology/Separation/NotNormal): generalize to non-separable spaces (#33414)

peakpoint
authored and
pfaffelh
committed
feat(Analysis/TemperedDistribution): derivatives (#32770)

mcdoll
authored and
pfaffelh
committed
feat(Analysis/TemperedDistribution): Fourier transform of the dirac delta (#33230)

mcdoll
authored and
pfaffelh
committed
doc(Analysis): fix file refs (#33451)

harahu
authored and
pfaffelh
committed
feat(Schwarz): add a version for maps with derivative zero (#33563)

authored and
pfaffelh
committed
feat(UnitDisc): define `Pow 𝔻 ℕ+` (#33630)

urkud
authored and
pfaffelh
committed
chore: adaptations for batteries#1588 (#33681)

authored and
pfaffelh
committed
chore: use `IsScalarTower.algebraMap_eq` to golf two proofs (#33353)

ocfnash
authored and
pfaffelh
committed
chore: deprecate duplicate results about `zsmul` (#33653)

vihdzp
authored and
pfaffelh
committed
chore(Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity): rename `.rfl` to `.refl` (#33673)

SnirBroshi
authored and
pfaffelh
committed
feat(Topology/Inseparable): condition for the compactness of a subset (#33678)

gasparattila
authored and
pfaffelh
committed
feat(AlgebraicGeometry): universal property of relative normalization (#33476)

erdOne
authored and
pfaffelh
committed
feat(RingTheory): quasi-finite algebras (#32665)

erdOne
authored and
pfaffelh
committed
perf(translate): only run `check` after kernel check fails (#33498)

JovanGerb
authored and
pfaffelh
committed
chore: update Mathlib dependencies 2026-01-07 (#33695)

authored and
pfaffelh
committed
chore(Topology/Order/Lattice): tag continuity lemmas with `fun_prop` (#33682)

gasparattila
authored and
pfaffelh
committed
chore(UnitDisc): review API (#33639)

urkud
authored and
pfaffelh
committed
chore(Order/Defs/Unbundled): deprecate `IsAntisymm` in favor of core's `Std.Antisymm` (#33685)

SnirBroshi
authored and
pfaffelh
committed
feat: Upgrade theorem `MeromorphicAt.comp_analyticAt` (#33703)

kebekus
authored and
pfaffelh
committed
feat: add Artinian schemes (#32412)

authored and
pfaffelh
committed
ci(daily.yml): remove continue-on-error from check steps (#33694)

bryangingechen
authored and
pfaffelh
committed
feat: a dense Gdelta subset of a Baire space is Baire. (#32674)

authored and
pfaffelh
committed
chore(Tactic/Translate/ToDual): fix typo in `nameDict` (#33701)

JovanGerb
authored and
pfaffelh
committed
feat(MeasureTheory): more MeasurableSMul -> MeasurableConstSMul (#33710)

loefflerd
authored and
pfaffelh
committed
chore: fix more spacing issues (#33705)

grunweg
authored and
pfaffelh
committed
feat(RingTheory): noetherian model for etale algebras (#32837)

erdOne
authored and
pfaffelh
committed
feat(Analysis): ℘ is analytic (#32911)

erdOne
authored and
pfaffelh
committed
feat: nontrivial instances for valuation with `ℤᵐ⁰` as codomain (#33060)

authored and
pfaffelh
committed
refactor(Combinatorics/SimpleGraph/VertexCover): assumes containment instead of injective hom (#33622)

vlad902
authored and
pfaffelh
committed
feat: more API for ae strongly measurable functions on compact sets (#33670)

sgouezel
authored and
pfaffelh
committed
feat(AlgebraicGeometry): fpqc descent implies fppf descent (#33556)

erdOne
authored and
pfaffelh
committed
chore: fix whitespace (#33629)

authored and
pfaffelh
committed
feat(Order): `OrderIso` involving `Prod` and `Lex` (#33663)

YanYablonovskiy
authored and
pfaffelh
committed
chore: remove some duplicate instances (#33667)

JovanGerb
authored and
pfaffelh
committed
chore: more `fun_prop` attributes and lemmas (#33671)

sgouezel
authored and
pfaffelh
committed
chore: fix more spacing issues (#33706)

grunweg
authored and
pfaffelh
committed
chore(AlgebraicGeometry/ProjectiveSpectrum): delete unused code (#33711)

Vierkantor
authored and
pfaffelh
committed
feat(RingTheory/Morita/Matrix): more on morita equivalence between `R` and `Mn(R)` (#32988)

authored and
pfaffelh
committed
feat(Polynomial/Derivative): formulas for iterated derivatives of P * X^m (#33306)

YuvalFilmus
authored and
pfaffelh
committed
chore: fix even more spacing issues (#33716)

grunweg
authored and
pfaffelh
committed
chore(MeasureTheory): remove redundant `by_cases` (#33725)

yuma-mizuno
authored and
pfaffelh
committed
feat: define `PolynormableSpace` (#32480)

ADedecker
authored and
pfaffelh
committed
feat(CategoryTheory): lifting colimit cocone to `Over` (#33536)

erdOne
authored and
pfaffelh
committed
fix(Tactic/DepRewrite): unknown free variable on `rw!` at local hypothesis (#33686)

plp127
authored and
pfaffelh
committed
feat(Analysis/Asymptotics): Adds Asymptotics.IsEquivalent.Log (#33522)

ajirving
authored and
pfaffelh
committed
chore(Topology/Covering): adjust some statements (#33721)

alreadydone
authored and
pfaffelh
committed
feat(Analysis/Distribution): more lemmas for temperate growth functions (#33597)

authored and
pfaffelh
committed
chore(Topology): fix whitespace (#33728)

harahu
authored and
pfaffelh
committed
feat(Analysis/SchwartzSpace): scalar multiplication with linear factors (#33404)

mcdoll
authored and
pfaffelh
committed
chore: rename the `commandStart` linter to `whitespace` (#33708)

grunweg
authored and
pfaffelh
committed
fix(ci): show helpful message when runLinter needs master merge (#33696)

kim-em
authored and
pfaffelh
committed
ci: add commit verification for transient commits (#33713)

jcommelin
authored and
pfaffelh
committed
chore(RingTheory): fix whitespace (#33729)

harahu
authored and
pfaffelh
committed
chore(CategoryTheory): fix whitespace (#33730)

harahu
authored and
pfaffelh
committed
style(misc): fix whitespace (#33732)

harahu
authored and
pfaffelh
committed
chore: update Mathlib dependencies 2026-01-07 (#33733)

authored and
pfaffelh
committed
ci(daily.yml): get job status from API instead of via needs context (#33738)

bryangingechen
authored and
pfaffelh
committed
fix(Cache): option order in usage & error messages (#33735)

tydeu
authored and
pfaffelh
committed
chore(Order/Defs/Unbundled): deprecate `IsIrrefl` in favor of core's `Std.Irrefl` (#33717)

SnirBroshi
authored and
pfaffelh
committed
feat(RingTheory/PowerSeries/Schroder): Define the generating function for large Schroder number (#30881)

authored and
pfaffelh
committed
feat(GroupTheory/SpecificGroups/Cyclic): generalize the proof of prime_card by not assuming Finite (#32152)

Lingyin00
authored and
pfaffelh
committed
chore(Analysis/InnerProductSpace): the Laplacian is `k`-linear (#33739)

mcdoll
authored and
pfaffelh
committed
feat(Topology): add definition for subpaths (#27261)

authored and
pfaffelh
committed
refactor: make `LinearOrderedCommMonoidWithZero`s cancellative (#31749)

YaelDillies
authored and
pfaffelh
committed
feat(RingTheory): some base changes commute with integral closure (#33553)

erdOne
authored and
pfaffelh
committed
chore(Algebra/Exact): refactor using `to_additive` (#33719)

tb65536
authored and
pfaffelh
committed
feat(FundamentalGroupoid/InducedMaps): generalize to different universes (#33445)

urkud
authored and
pfaffelh
committed
feat(to_dual): `to_dual none` to have the dual as an implementation detail (#33497)

JovanGerb
authored and
pfaffelh
committed
chore: update Mathlib dependencies 2026-01-08 (#33742)

authored and
pfaffelh
committed
feat(ModelTheory/Definability): TermDefinable functions (#26332)

Timeroot
authored and
pfaffelh
committed
feat(Powerset): Results related to image (#33193)

YuvalFilmus
authored and
pfaffelh
committed
chore: use a generic neighborhood instead of balls in theorems on parametric integrals (#33460)

sgouezel
authored and
pfaffelh
committed
feat(AlgebraicGeometry): properties of `coprod.map` and `coprod.desc` (#33472)

erdOne
authored and
pfaffelh
committed
feat(Topology): trivial lemmas (#33720)

alreadydone
authored and
pfaffelh
committed
chore(Algebra/GroupWithZero): deprecate `mul_mem_nonZeroDivisors{Left,Right}_of_mem_nonZeroDivisors{Left,Right}` (#33734)

euprunin
authored and
pfaffelh
committed
feat: Matrix.IsSymm.inv (#33748)

Ruben-VandeVelde
authored and
pfaffelh
committed
fix: generalize ContinuousLinearMap.map_add₂ and friends (#33750)

eric-wieser
authored and
pfaffelh
committed
chore(Archive,Counterexamples): find whitespace (#33759)

grunweg
authored and
pfaffelh
committed
chore: remove superfluous disabling of the whitespace linter (#33758)

grunweg
authored and
pfaffelh
committed
feat: add IsNowhereDense helpers (#32740)

LTolDe
authored and
pfaffelh
committed
chore(Tactic): remove duplicate instances (#33666)

JovanGerb
authored and
pfaffelh
committed
feat(DifferentialForm): exterior derivative applied to vector fields (#30886)

authored and
pfaffelh
committed
feat: IMO 2010 Q5 (#31315)

Parcly-Taxel
authored and
pfaffelh
committed
fix(Tactic/TacticAnalysis): analyze tactics inside `have ... := by ...` (#33584)

kim-em
authored and
pfaffelh
committed
fix: `simp_rw` does not hide goals (#32956)

adomani
authored and
pfaffelh
committed
feat: uniqueness API for implicit function of `IsContDiffImplicitAt` (#31988)

winstonyin
authored and
pfaffelh
committed
feat: some lemmas about finsum/finprod (#33186)

authored and
pfaffelh
committed
feat(Algebra/Algebra/Subalgebra): remove unnecessary assumptions in `iSup_induction` and `iSup_induction'` (#33674)

euprunin
authored and
pfaffelh
committed
chore: tidy various files (#33687)

Ruben-VandeVelde
authored and
pfaffelh
committed
ci: wrap linting with stdbuf -oL so log output appears immediately (#33783)

bryangingechen
authored and
pfaffelh
committed
doc(Algebra): fix file refs (#33620)

harahu
authored and
pfaffelh
committed
feat: more API for upper hemicontinuous functions (#33626)

j-loreaux
authored and
pfaffelh
committed
fix: Rename constructors in Irrational.lean docstrings (#33524)

ldct
authored and
pfaffelh
committed
feat: Schur's lemma over an algebraically closed field (#33216)

authored and
pfaffelh
committed
feat(MeasureTheory): interval integral is absolutely continuous (#32163)

zhuyizheng
authored and
pfaffelh
committed
chore: fix whitespace (#33747)

harahu
authored and
pfaffelh
committed
chore(Order/Defs/Unbundled): deprecate `IsRefl` in favor of core's `Std.Refl` (#33755)

SnirBroshi
authored and
pfaffelh
committed
feat: a lower bound for the volume of a cone on the unit sphere (#31960)

urkud
authored and
pfaffelh
committed
feat(ConvexSpace): complete `proof_wanted` statements (#33562)

kim-em
authored and
pfaffelh
committed
fix(translate): don't unfold aux lemmas, but translate them (#33603)

JovanGerb
authored and
pfaffelh
committed
refactor: unify the two versions of `pow_eq_one_iff` (#30799)

YaelDillies
authored and
pfaffelh
committed
feat(Topology.GDelta.Basic): add helpers for IsMeagre (#33308)

LTolDe
authored and
pfaffelh
committed
feat(Combinatorics/SimpleGraph): distributivity of box product over sum (#32238)

YaelDillies
authored and
pfaffelh
committed
cs0

pfaffelh
authored and
pfaffelh
committed
Update Mathlib.lean

pfaffelh
and
github-actions[bot]
committed

Commits on Jan 17, 2026

chore: clean up porting note left after #28324 (#28742)

bryangingechen
authored and
pfaffelh
committed
doc: fix repeated typo "nonegative" (#29637)

harahu
authored and
pfaffelh
committed