Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-26 12:02 32b08ef8

View on Github →

feat: add_monoid_with_one, add_group_with_one (#12182) Adds two type classes add_monoid_with_one R and add_group_with_one R with operations for ℕ → R and ℤ → R, resp. The type classes extend add_monoid and add_group because those seem to be the weakest type classes where such a +₀₁-homomorphism is guaranteed to exist. The nat.cast function as well as coe : ℕ → R are implemented in terms of add_monoid_with_one R, removing the infamous nat.cast diamond. Fixes #946. Some lemmas are less general now because the algebraic hierarchy is not fine-grained enough, or because the lawful coercion only exists for monoids and above. This generality was not used in mathlib as far as I could tell. For example:

  • char_p.char_p_to_char_zero now requires a group instead of a left-cancellative monoid, because we don't have the add_left_cancel_monoid_with_one class
  • nat.norm_cast_le now requires a seminormed ring instead of a seminormed group, because we don't have semi_normed_group_with_one

Estimated changes

modified theorem int.cast_list_sum
modified theorem int.cast_multiset_sum
modified theorem int.cast_sum
modified theorem nat.cast_list_sum
modified theorem nat.cast_multiset_sum
modified theorem nat.cast_sum
modified theorem char_p.cast_card_eq_zero
modified theorem char_p.cast_eq_zero
modified theorem char_p.char_p_to_char_zero
modified theorem char_p.congr
modified theorem char_p.eq
modified theorem char_p.int_cast_eq_zero_iff
deleted theorem char_zero_of_inj_zero
deleted theorem nat.cast_add_one_ne_zero
deleted theorem nat.cast_eq_one
deleted theorem nat.cast_eq_zero
deleted theorem nat.cast_inj
deleted theorem nat.cast_injective
deleted theorem nat.cast_ne_one
deleted theorem nat.cast_ne_zero
added theorem char_zero_of_inj_zero
added theorem nat.cast_eq_one
added theorem nat.cast_eq_zero
added theorem nat.cast_inj
added theorem nat.cast_injective
added theorem nat.cast_ne_one
added theorem nat.cast_ne_zero
added theorem direct_sum.of_int_cast
added theorem direct_sum.of_nat_cast
modified theorem nsmul_one
modified theorem zsmul_eq_mul
modified theorem zsmul_one
modified theorem char_zero.of_module
modified theorem ne_zero.ne'
modified theorem ne_zero.not_char_dvd
modified theorem ne_zero.of_ne_zero_coe
modified theorem ne_zero.of_not_dvd
modified theorem ne_zero.pos_of_ne_zero_coe
modified theorem int.ceil_pos
modified theorem int.ceil_zero
modified theorem int.floor_add_nat
modified theorem int.floor_nat_add
modified theorem int.floor_nonneg
modified theorem int.floor_sub_nat
modified theorem int.floor_zero
modified theorem nat.ceil_eq_zero
modified theorem nat.ceil_zero
modified theorem nat.floor_zero
modified theorem nat.lt_floor_add_one
added theorem nat.strict_mono_cast
added theorem nat.norm_cast_le
deleted theorem nat.norm_cast_le
modified theorem int.coe_nat_abs
modified theorem int.coe_nat_eq_zero
modified theorem int.coe_nat_ne_zero
modified theorem int.coe_nat_nonneg
modified theorem int.coe_nat_pos
added theorem int.neg_of_nat_ne_zero
added theorem int.zero_ne_neg_of_nat
deleted theorem int.cast_add
modified def int.cast_add_hom
deleted theorem int.cast_bit0
deleted theorem int.cast_bit1
deleted theorem int.cast_coe_nat'
deleted theorem int.cast_coe_nat
modified theorem int.cast_commute
deleted theorem int.cast_four
modified theorem int.cast_ite
modified theorem int.cast_mul
deleted theorem int.cast_neg
added theorem int.cast_neg_nat_cast
deleted theorem int.cast_neg_of_nat
deleted theorem int.cast_neg_succ_of_nat
deleted theorem int.cast_of_nat
deleted theorem int.cast_one
deleted theorem int.cast_sub
deleted theorem int.cast_sub_nat_nat
deleted theorem int.cast_three
deleted theorem int.cast_two
deleted theorem int.cast_zero
modified theorem int.coe_cast_add_hom
deleted theorem int.coe_nat_bit0
deleted theorem int.coe_nat_bit1
deleted theorem int.nat_cast_eq_coe_nat
modified theorem mul_opposite.op_int_cast
modified theorem mul_opposite.unop_int_cast
modified theorem pi.coe_int
modified theorem pi.int_apply
modified theorem prod.fst_int_cast
modified theorem prod.snd_int_cast
added theorem int.cast_add
added theorem int.cast_bit0
added theorem int.cast_bit1
added theorem int.cast_coe_nat
added theorem int.cast_four
added theorem int.cast_neg
added theorem int.cast_neg_of_nat
added theorem int.cast_of_nat
added theorem int.cast_one
added theorem int.cast_sub
added theorem int.cast_sub_nat_nat
added theorem int.cast_three
added theorem int.cast_two
added theorem int.cast_zero
added theorem int.coe_nat_bit0
added theorem int.coe_nat_bit1
added theorem int.neg_of_nat_eq
added theorem nat.cast_pred
added theorem nat.cast_sub
modified theorem int.cast_eq_zero
modified theorem int.cast_inj
modified theorem int.cast_injective
modified theorem int.cast_ne_zero
modified theorem add_monoid_hom.ext_nat
modified theorem ext_nat'
modified theorem map_nat_cast'
modified theorem mul_opposite.op_nat_cast
modified theorem mul_opposite.unop_nat_cast
deleted theorem nat.bin_cast_eq
deleted theorem nat.cast_add
deleted theorem nat.cast_add_one
deleted theorem nat.cast_bit0
deleted theorem nat.cast_bit1
deleted theorem nat.cast_ite
modified theorem nat.cast_mul
modified theorem nat.cast_nonneg
deleted theorem nat.cast_one
deleted theorem nat.cast_pred
modified theorem nat.cast_ring_hom_nat
deleted theorem nat.cast_sub
deleted theorem nat.cast_succ
deleted theorem nat.cast_two
modified theorem nat.cast_with_bot
deleted theorem nat.cast_zero
modified theorem nat.coe_cast_add_monoid_hom
deleted theorem nat.strict_mono_cast
modified theorem pi.coe_nat
modified theorem pi.nat_apply
added theorem nat.bin_cast_eq
added theorem nat.cast_add
added theorem nat.cast_add_one
added theorem nat.cast_bit0
added theorem nat.cast_bit1
added theorem nat.cast_ite
added theorem nat.cast_one
added theorem nat.cast_succ
added theorem nat.cast_two
added theorem nat.cast_zero
modified theorem enat.coe_inj
modified theorem enat.dom_coe
modified theorem enat.some_eq_coe
added theorem num.add_of_nat'
modified theorem num.add_of_nat
added theorem num.bit1_succ
modified theorem num.cast_of_znum
modified theorem num.cast_sub'
modified theorem num.cast_succ'
modified theorem num.cast_succ
modified theorem num.cast_to_int
modified theorem num.cast_to_nat
added theorem num.of_int'_to_znum
added theorem num.of_nat'_bit
added theorem num.of_nat'_one
added theorem num.of_nat'_succ
modified theorem num.of_nat'_zero
modified theorem num.of_nat_cast
modified theorem num.of_nat_inj
deleted theorem num.of_nat_to_znum
deleted theorem num.of_nat_to_znum_neg
added theorem num.of_to_nat'
modified theorem num.of_to_nat
added theorem num.pred_succ
added theorem num.succ_of_int'
added theorem num.to_znum_neg_succ
added theorem num.to_znum_succ
modified theorem pos_num.cast_add
modified theorem pos_num.cast_inj
modified theorem pos_num.cast_sub'
modified theorem pos_num.cast_succ
modified theorem pos_num.cast_to_int
modified theorem pos_num.cast_to_nat
added theorem pos_num.of_to_nat'
modified theorem pos_num.of_to_nat
modified theorem znum.cast_add
modified theorem znum.cast_bit0
modified theorem znum.cast_bit1
modified theorem znum.cast_bitm1
added theorem znum.cast_sub
modified theorem znum.cast_succ
modified theorem znum.cast_to_int
modified theorem znum.of_int'_eq
added theorem znum.of_int'_neg
modified theorem znum.of_int_cast
modified theorem znum.of_nat_cast
added theorem znum.of_nat_to_znum
added theorem znum.of_to_int'
modified theorem znum.of_to_int
modified theorem znum.to_of_int
modified theorem rat.cast_coe_nat
modified theorem rat.coe_int_eq_mk
modified theorem irrational.ne_zero
added theorem sphere_ext_iff
added theorem stereographic_apply
modified theorem lucas_lehmer.X.int_coe_fst
modified theorem lucas_lehmer.X.int_coe_snd
modified theorem lucas_lehmer.X.nat_coe_fst
modified theorem lucas_lehmer.X.nat_coe_snd
modified theorem zsqrtd.coe_nat_im
modified theorem zsqrtd.coe_nat_re
modified theorem zsqrtd.coe_nat_val
added theorem nat_cast_mem
deleted def witt_vector.map
deleted theorem pgame.nat_one