Commit 2026-07-21 21:41 6421d4ee

View on Github →

chore: fix argument names of MonoidAlgebra.induction_on (#41900) Fix argument names for MonoidAlgebra.induction_on and AddMonoidAlgebra.induction_on and MonoidAlgebra.induction_linear. Name the motive motive and name the minor premises according to their contents.

Estimated changes

Modified Mathlib/Algebra/MonoidAlgebra/Defs.lean

modified theorem AddMonoidAlgebra.induction_on

modified theorem MonoidAlgebra.induction_linear

modified theorem MonoidAlgebra.induction_on

Modified Mathlib/RepresentationTheory/Basic.lean

Modified Mathlib/RingTheory/FiniteType.lean