Commit 2026-03-15 14:55 2d206e33

View on Github →

chore: rename Ordinal.smul_eq_mul → Ordinal.nsmul_eq_mul (#36669) And make it a simp lemma too.

Estimated changes

added theorem Ordinal.nsmul_eq_mul
deleted theorem Ordinal.smul_eq_mul