Commit 2025-01-13 12:45 c485bfa9
View on Github →chore: review induction principles for Set.Finite (#20444)
Rename Set.Finite.dinduction_on to Set.Finite.induction_on as this is the more useful induction principle (it works with induction). Rename Set.Finite.induction_on' to Set.Finite.induction_on_subset and make it dependent. Give the assumptions meaningful names.