Commit 2024-11-13 20:45 ad323cc0

View on Github →

chore: name the argument to IsWellFounded.induction (#18993) ... so that it can be named with induction From GrowthInGroups

Estimated changes

Modified Mathlib/Order/RelClasses.lean

modified theorem IsWellFounded.induction

modified theorem WellFoundedGT.induction

modified theorem WellFoundedLT.induction