Theorem Ordinal.card_one

Modification history

2023-08-06 20:21
Mathlib/SetTheory/Ordinal/Basic.lean
feat: change definition of natCast in Cardinal to lift #(Fin n) (#6384) …
Modified Ordinal.card_oneView on Github →
2023-02-13 06:43
Mathlib/SetTheory/Ordinal/Basic.lean
feat: port SetTheory.Ordinal.Basic (#2217) …
Added Ordinal.card_oneView on Github →