Commit 2024-09-18 16:52 a5f29991

View on Github →

chore(SetTheory/Ordinal/NaturalOps): fix argument implicitness (#16900)

Estimated changes

modified theorem NatOrdinal.toOrdinal_eq_one
modified theorem NatOrdinal.toOrdinal_max
modified theorem NatOrdinal.toOrdinal_min