Commit 2024-12-20 06:52 8854cbcb

View on Github →

chore: further backports for leanprover/lean4#6397 (#20098)

Estimated changes

Modified Mathlib/Algebra/FreeMonoid/Count.lean

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean

Modified Mathlib/CategoryTheory/Functor/OfSequence.lean

Modified Mathlib/Combinatorics/Quiver/SingleObj.lean

Modified Mathlib/Computability/PartrecCode.lean

modified theorem Nat.Partrec.Code.eval_curry

modified theorem Nat.Partrec.Code.eval_id

Modified Mathlib/Computability/RegularExpressions.lean

Modified Mathlib/Computability/TMToPartrec.lean

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/List/DropRight.lean

Modified Mathlib/Data/List/EditDistance/Defs.lean

Modified Mathlib/Data/List/Indexes.lean

Modified Mathlib/Data/List/Range.lean

Modified Mathlib/Data/Nat/Multiplicity.lean

Modified Mathlib/Data/Num/Lemmas.lean

Modified Mathlib/Data/Ordmap/Ordset.lean

Modified Mathlib/Data/TypeVec.lean

Modified Mathlib/Data/W/Constructions.lean

Modified Mathlib/Deprecated/LazyList.lean

Modified Mathlib/GroupTheory/CoprodI.lean

Modified Mathlib/GroupTheory/Coxeter/Inversion.lean

Modified Mathlib/ModelTheory/Algebra/Field/IsAlgClosed.lean

Modified Mathlib/ModelTheory/Semantics.lean

Modified Mathlib/RingTheory/FractionalIdeal/Basic.lean

Modified Mathlib/SetTheory/ZFC/Basic.lean

added theorem PSet.empty_def

Modified Mathlib/SetTheory/ZFC/Rank.lean

modified theorem PSet.rank_empty

Modified Mathlib/Topology/Category/Profinite/Nobeling.lean