Commit 2026-02-28 15:12 24cb29a8

View on Github →

chore(SetTheory/Ordinal/Arithmetic): avoid terminal simp only (#35854) As per convention. Plus other small stylistic changes around Ordinal.mod.

Estimated changes

modified theorem Ordinal.mod_lt
modified theorem Ordinal.mod_one
modified theorem Ordinal.mod_self
modified theorem Ordinal.mod_zero
modified theorem Ordinal.zero_mod