Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-07-16 07:50 31b269b6

View on Github →

feat(set_theory/ordinal/natural_ops): define natural multiplication (#14324)

Estimated changes

Modified src/set_theory/ordinal/arithmetic.lean

added def ordinal.blsub₂

added theorem ordinal.lt_blsub₂

Modified src/set_theory/ordinal/natural_ops.lean

added theorem nat_ordinal.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.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_lt_nadd_of_le_of_lt

added theorem ordinal.nadd_lt_nadd_of_lt_of_le

added theorem ordinal.nadd_nmul

added theorem ordinal.nadd_one_nmul

added theorem ordinal.nadd_right_comm

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_le_iff₃

added theorem ordinal.nmul_le_nmul_of_nonneg_left

added theorem ordinal.nmul_le_nmul_of_nonneg_right

added theorem ordinal.nmul_lt_nmul_of_pos_left

added theorem ordinal.nmul_lt_nmul_of_pos_right

added theorem ordinal.nmul_nadd

added theorem ordinal.nmul_nadd_le

added theorem ordinal.nmul_nadd_le₃'

added theorem ordinal.nmul_nadd_le₃

added theorem ordinal.nmul_nadd_lt

added theorem ordinal.nmul_nadd_lt₃'

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.to_nat_ordinal_max

modified theorem ordinal.to_nat_ordinal_min

added theorem ordinal.zero_nmul

Modified src/set_theory/ordinal/principal.lean

deleted def ordinal.blsub₂

deleted theorem ordinal.lt_blsub₂