Theorem Cardinal.ord_inj

Modification history

2026-05-18 12:33
Mathlib/SetTheory/Ordinal/Basic.lean
chore: review `Cardinal.ord` API (#35865) …
Modified Cardinal.ord_injView on Github →
2024-09-18 21:33
Mathlib/SetTheory/Ordinal/Basic.lean
feat(SetTheory/Ordinal/Basic): added ord_zero_iff lemma (#16912) …
Added Cardinal.ord_injView on Github →