Commit 2026-03-21 21:14 a0b56123

View on Github →

chore: rename arguments of Cardinal.inductionOn (#36929) So we can use as induction c using Cardinal.inductionOn with | mk α.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Defs.lean

modified theorem Cardinal.inductionOn

modified theorem Cardinal.inductionOn₂

modified theorem Cardinal.inductionOn₃

modified theorem Cardinal.induction_on_pi