Commit 2024-12-15 23:28 00a4da3d

View on Github →

chore(SetTheory/Ordinal/NaturalOps): address porting notes (#19237) We also private/deprecate some primed lemmas which are really only useful to prove associativity of multiplication.

Estimated changes

Modified Mathlib/SetTheory/Ordinal/NaturalOps.lean

modified theorem NatOrdinal.toOrdinal_toNatOrdinal

modified theorem Ordinal.lt_nmul_iff₃'

modified theorem Ordinal.lt_nmul_iff₃

deleted theorem Ordinal.nmul_le_iff₃'

modified theorem Ordinal.nmul_le_iff₃

deleted theorem Ordinal.nmul_nadd_lt₃'

modified theorem Ordinal.toNatOrdinal_toOrdinal