Commit 2026-02-06 16:14 0e1651d8

View on Github →

chore(Order/RelClasses): name arguments of recursors (#33905) Name the motive motive and name the minor premises something descriptive.

Estimated changes

Modified Mathlib/Order/RelClasses.lean

modified def IsWellFounded.fix

modified theorem IsWellFounded.fix_eq

modified theorem IsWellFounded.induction

modified def WellFoundedLT.fix

modified theorem WellFoundedLT.fix_eq