Commit 2026-03-10 13:37 fbc91858

View on Github →

chore: fix induction and recursor names (#35884)

Finset.induction_on_{min,max}, Finset.induction_on_{min,max}_value
FreeAbelianGroup.induction_on, FreeAbelianGroup.induction_on' Applications of these induction principles are also fixed.

Estimated changes

Modified Mathlib/Algebra/Order/Rearrangement.lean

Modified Mathlib/Combinatorics/Additive/SubsetSum.lean

Modified Mathlib/Data/Finset/Max.lean

modified theorem Finset.induction_on_max

modified theorem Finset.induction_on_max_value

modified theorem Finset.induction_on_min

modified theorem Finset.induction_on_min_value

Modified Mathlib/GroupTheory/FreeAbelianGroup.lean

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean