Theorem Ordinal.inductionOnWellOrder

Modification history

2026-03-22 11:57

Mathlib/SetTheory/Ordinal/Basic.lean

chore: rename arguments of `Ordinal.inductionOn` (#36977) …

Modified Ordinal.inductionOnWellOrder View on Github →

2024-12-12 20:12

Mathlib/SetTheory/Ordinal/Basic.lean

feat(SetTheory/Ordinal/Basic): recursion on well-orders (#19678) …

Added Ordinal.inductionOnWellOrder View on Github →