Theorem Ordinal.inductionOn₂

Modification history

2026-03-22 11:57
Mathlib/SetTheory/Ordinal/Basic.lean
chore: rename arguments of `Ordinal.inductionOn` (#36977) …
Modified Ordinal.inductionOn₂View on Github →
2024-10-10 02:53
Mathlib/SetTheory/Ordinal/Basic.lean
chore(SetTheory/Ordinal/Basic): golf various instances (#17527)
Added Ordinal.inductionOn₂View on Github →