Commit 2024-03-25 02:18 f2f41de1

View on Github →

chore: rm @[eqns] in SetTheory/Ordinal/Notation (#11646)

Estimated changes

modified theorem ONote.ofNat_succ
modified theorem ONote.ofNat_zero