Commit 2025-04-03 17:18 08f9285c

View on Github →

chore: fix more induction branch names (#23448) Follow-up to #23358. This includes changing the name of the motive variable to motive and naming branches as if they were lemmas. The regex used for finding the branch names was ^\s+\| [hH][^:]*? =>.

Estimated changes

modified theorem Submonoid.closure_induction
modified theorem Submonoid.dense_induction
modified theorem Submonoid.iSup_induction'
modified theorem Submonoid.iSup_induction
modified theorem LieSubmodule.iSup_induction
modified theorem Finset.cons_induction
modified theorem Finset.cons_induction_on
modified theorem Finset.induction_on'
modified theorem Finsupp.induction_linear
modified theorem Finsupp.induction₂
modified theorem Submodule.iSup_induction'
modified theorem Submodule.iSup_induction