Commit 2023-07-18 05:18 a3e15d84

View on Github →

chore: forward port #14324 (#5973) This is the remainder of the forward port of https://github.com/leanprover-community/mathlib/pull/14324. See https://leanprover-community.github.io/mathlib-port-status/file/set_theory/ordinal/natural_ops for the relevant #outofsync page.

Estimated changes

added theorem NatOrdinal.mul_le_nmul
added theorem Ordinal.add_one_nmul
added theorem Ordinal.le_nadd_left
added theorem Ordinal.le_nadd_right
added theorem Ordinal.le_nadd_self
added theorem Ordinal.le_self_nadd
added theorem Ordinal.lt_nmul_iff
added theorem Ordinal.lt_nmul_iff₃
added theorem Ordinal.nadd_eq_add
added theorem Ordinal.nadd_le_nadd
added theorem Ordinal.nadd_left_comm
added theorem Ordinal.nadd_lt_nadd
added theorem Ordinal.nadd_nmul
added theorem Ordinal.nadd_one_nmul
added theorem Ordinal.nmul_add_one
added theorem Ordinal.nmul_assoc
added theorem Ordinal.nmul_comm
added theorem Ordinal.nmul_def
added theorem Ordinal.nmul_eq_mul
added theorem Ordinal.nmul_le_iff
added theorem Ordinal.nmul_le_iff₃
added theorem Ordinal.nmul_nadd
added theorem Ordinal.nmul_nadd_le
added theorem Ordinal.nmul_nadd_lt
added theorem Ordinal.nmul_nadd_one
added theorem Ordinal.nmul_nonempty
added theorem Ordinal.nmul_one
added theorem Ordinal.nmul_succ
added theorem Ordinal.nmul_zero
added theorem Ordinal.one_nmul
added theorem Ordinal.succ_nmul
modified theorem Ordinal.toNatOrdinal_max
modified theorem Ordinal.toNatOrdinal_min
added theorem Ordinal.zero_nmul