Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-23 10:06 0abe0860

View on Github →

feat(data/ordinal): mul, div, mod, dvd, sub, power

Estimated changes

Modified algebra/linear_algebra/basic.lean

Modified data/cardinal.lean

added theorem cardinal.le_zero

added theorem cardinal.omega_ne_zero

Modified data/equiv.lean

added theorem equiv.prod_assoc_apply

added theorem equiv.prod_sum_distrib_apply_left

added theorem equiv.prod_sum_distrib_apply_right

added theorem equiv.prod_unit_apply

added theorem equiv.sum_prod_distrib_apply_left

added theorem equiv.sum_prod_distrib_apply_right

added theorem equiv.unit_prod_apply

Modified data/ordinal.lean

added theorem cardinal.add_one_of_omega_le

added theorem cardinal.ord_is_limit

added theorem ordinal.add_is_limit

added theorem ordinal.add_le_of_limit

added theorem ordinal.add_sub_cancel_of_le

added theorem ordinal.card_mul

added theorem ordinal.card_succ

added theorem ordinal.div_add_mod

added def ordinal.div_def

added theorem ordinal.div_eq_zero_of_lt

added theorem ordinal.div_le

added theorem ordinal.div_le_of_le_mul

added theorem ordinal.div_lt

added theorem ordinal.div_mul_cancel

added theorem ordinal.div_one

added theorem ordinal.div_self

added theorem ordinal.div_zero

added theorem ordinal.dvd_def

added theorem ordinal.dvd_mul

added theorem ordinal.dvd_zero

added theorem ordinal.le_div

added theorem ordinal.le_of_mul_le_mul_left

added theorem ordinal.le_succ_of_is_limit

added theorem ordinal.le_zero

added theorem ordinal.limit_le

added theorem ordinal.limit_rec_on_limit

added theorem ordinal.limit_rec_on_succ

added theorem ordinal.limit_rec_on_zero

added theorem ordinal.lt_div

added theorem ordinal.lt_mul_div_add

added theorem ordinal.lt_mul_succ_div

added theorem ordinal.lt_succ

added theorem ordinal.mod_def

added theorem ordinal.mod_eq_of_lt

added theorem ordinal.mod_lt

added theorem ordinal.mod_one

added theorem ordinal.mod_self

added theorem ordinal.mod_zero

added theorem ordinal.mul_add

added theorem ordinal.mul_add_div

added theorem ordinal.mul_assoc

added theorem ordinal.mul_div_cancel

added theorem ordinal.mul_div_le

added theorem ordinal.mul_is_limit

added theorem ordinal.mul_le_mul_iff_left

added theorem ordinal.mul_le_mul_left

added theorem ordinal.mul_le_mul_right

added theorem ordinal.mul_le_of_limit

added theorem ordinal.mul_left_inj

added theorem ordinal.mul_lt_mul_iff_left

added theorem ordinal.mul_lt_mul_of_pos_left

added theorem ordinal.mul_lt_of_lt_div

added theorem ordinal.mul_one

added theorem ordinal.mul_pos

added theorem ordinal.mul_succ

added theorem ordinal.mul_zero

added theorem ordinal.not_succ_is_limit

added theorem ordinal.not_succ_of_is_limit

added theorem ordinal.one_add_of_omega_le

added theorem ordinal.one_add_omega

added theorem ordinal.one_dvd

added theorem ordinal.one_eq_lift_type_unit

added theorem ordinal.one_eq_type_unit

added theorem ordinal.one_mul

added theorem ordinal.pos_iff_ne_zero

added def ordinal.power

added theorem ordinal.power_le_of_limit

added theorem ordinal.power_limit

added theorem ordinal.power_succ

added theorem ordinal.power_zero

added theorem ordinal.sub_le_self

added theorem ordinal.sub_self

added theorem ordinal.sub_zero

added theorem ordinal.succ_lt_of_is_limit

added theorem ordinal.type_add

added theorem ordinal.type_eq_zero_iff_empty

added theorem ordinal.type_mul

added theorem ordinal.typein_apply

added theorem ordinal.zero_div

added theorem ordinal.zero_dvd

added theorem ordinal.zero_eq_lift_type_empty

added theorem ordinal.zero_eq_type_empty

added theorem ordinal.zero_mod

added theorem ordinal.zero_mul

added theorem ordinal.zero_sub

Modified data/prod.lean

added theorem prod.lex_def

Modified data/set/countable.lean

Modified data/set/lattice.lean

Modified data/sigma/basic.lean

added theorem subtype.mk_eq_mk

Modified data/sum.lean

added theorem sum.inl_ne_inr

added theorem sum.inr_ne_inl

Modified order/basic.lean

deleted def empty_relation.is_well_order

Modified order/order_iso.lean

added theorem order_embedding.nat_gt

added theorem subrel.order_embedding_apply

added theorem subrel_val