Commit 2026-07-24 17:51 3b3581ac

View on Github →

fix(Algebra/FreeMonoid): fix recursor argument names (#41929) Fix the argument names of FreeMonoid.recOn, FreeMonoid.inductionOn, and FreeMonoid.inductionOn'. Name the motive motive and name the minor premises according to their contents.

Estimated changes

modified def FreeMonoid.casesOn
modified theorem FreeMonoid.casesOn_of_mul
modified theorem FreeMonoid.casesOn_one
modified def FreeMonoid.recOn
modified theorem FreeMonoid.recOn_of_mul
modified theorem FreeMonoid.recOn_one