Theorem ONote.ofNat_one

Modification history

2025-01-05 03:32
Mathlib/SetTheory/Ordinal/Notation.lean
chore: bump toolchain to v4.16.0-rc1, and merge bump/v4.16.0 (#20464)
Modified ONote.ofNat_oneView on Github →
2023-06-21 05:19
Mathlib/SetTheory/Ordinal/Notation.lean
feat: port SetTheory.Ordinal.Notation (#2470)
Added ONote.ofNat_oneView on Github →