Commit 2025-09-11 07:19 212a45c4

View on Github →

chore: deprime induction in assorted files (#29291)

The rest of Algebra, except three instances in Algebra.Polynomial.EraseLead and Algebra.Polynomial.Laurent where induction branch names have to be fixed as well (this is done in #29537)
The rest of RingTheory
Everything outside the Algebra, Data, RingTheory folders (i.e. those instances that appeared after my "first round" of depriming)

Estimated changes

Modified Archive/Kuratowski.lean

Modified Mathlib/Algebra/Group/ForwardDiff.lean

Modified Mathlib/Algebra/Polynomial/BigOperators.lean

Modified Mathlib/Algebra/Polynomial/Degree/Lemmas.lean

Modified Mathlib/Algebra/Polynomial/Derivative.lean

Modified Mathlib/Algebra/Polynomial/Eval/Defs.lean

Modified Mathlib/Algebra/Polynomial/HasseDeriv.lean

Modified Mathlib/Algebra/Polynomial/Module/Basic.lean

Modified Mathlib/Algebra/Polynomial/Reverse.lean

modified theorem Polynomial.reflect_mul_induction

Modified Mathlib/Analysis/Complex/Exponential.lean

Modified Mathlib/Analysis/Real/Cardinality.lean

Modified Mathlib/Analysis/Real/Pi/Wallis.lean

Modified Mathlib/Combinatorics/Enumerative/Stirling.lean

Modified Mathlib/Combinatorics/Quiver/Path/Decomposition.lean

Modified Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean

Modified Mathlib/Dynamics/Ergodic/MeasurePreserving.lean

Modified Mathlib/Geometry/Manifold/ContMDiff/Basic.lean

Modified Mathlib/LinearAlgebra/Vandermonde.lean

Modified Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean

Modified Mathlib/RingTheory/Nilpotent/Basic.lean

Modified Mathlib/RingTheory/Norm/Transitivity.lean

Modified Mathlib/RingTheory/OreLocalization/Basic.lean

Modified Mathlib/RingTheory/OreLocalization/NonZeroDivisors.lean

Modified Mathlib/RingTheory/OreLocalization/Ring.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/TsumUniformlyOn.lean

Modified Mathlib/Topology/Order/HullKernel.lean

Modified MathlibTest/propose.lean