Commit 2023-03-18 07:59 c9e6ed71

View on Github →

feat: port RingTheory.Multiplicity (#2962)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Multiplicity.lean

added def multiplicity.Finite

added theorem multiplicity.Finset.prod

added theorem multiplicity.Int.coe_nat_multiplicity

added theorem multiplicity.Int.natAbs

added theorem multiplicity.addValuation_apply

added theorem multiplicity.dvd_iff_multiplicity_pos

added theorem multiplicity.dvd_of_multiplicity_pos

added theorem multiplicity.eq_coe_iff

added theorem multiplicity.eq_of_associated_left

added theorem multiplicity.eq_of_associated_right

added theorem multiplicity.eq_top_iff

added theorem multiplicity.eq_top_iff_not_finite

added theorem multiplicity.exists_eq_pow_mul_and_not_dvd

added theorem multiplicity.finite_def

added theorem multiplicity.finite_iff_dom

added theorem multiplicity.finite_mul

added theorem multiplicity.finite_mul_aux

added theorem multiplicity.finite_mul_iff

added theorem multiplicity.finite_nat_iff

added theorem multiplicity.finite_of_finite_mul_left

added theorem multiplicity.finite_of_finite_mul_right

added theorem multiplicity.finite_pow

added theorem multiplicity.get_multiplicity_self

added theorem multiplicity.get_one_right

added theorem multiplicity.isUnit_left

added theorem multiplicity.isUnit_right

added theorem multiplicity.is_greatest'

added theorem multiplicity.is_greatest

added theorem multiplicity.le_multiplicity_of_pow_dvd

added theorem multiplicity.lt_top_iff_finite

added theorem multiplicity.min_le_multiplicity_add

added theorem multiplicity.multiplicity_add_eq_min

added theorem multiplicity.multiplicity_add_of_gt

added theorem multiplicity.multiplicity_eq_multiplicity_iff

added theorem multiplicity.multiplicity_eq_zero

added theorem multiplicity.multiplicity_le_multiplicity_iff

added theorem multiplicity.multiplicity_le_multiplicity_of_dvd_left

added theorem multiplicity.multiplicity_le_multiplicity_of_dvd_right

added theorem multiplicity.multiplicity_lt_iff_neg_dvd

added theorem multiplicity.multiplicity_mk_eq_multiplicity

added theorem multiplicity.multiplicity_ne_zero

added theorem multiplicity.multiplicity_pow_self

added theorem multiplicity.multiplicity_pow_self_of_prime

added theorem multiplicity.multiplicity_self

added theorem multiplicity.multiplicity_sub_of_gt

added theorem multiplicity.multiplicity_zero_eq_zero_of_ne_zero

added theorem multiplicity.ne_top_iff_finite

added theorem multiplicity.ne_zero_of_finite

added theorem multiplicity.not_dvd_one_of_finite_one_right

added theorem multiplicity.not_finite_iff_forall

added theorem multiplicity.not_unit_of_finite

added theorem multiplicity.one_left

added theorem multiplicity.one_right

added theorem multiplicity.pos_of_dvd

added theorem multiplicity.pow

added theorem multiplicity.pow_dvd_iff_le_multiplicity

added theorem multiplicity.pow_dvd_of_le_multiplicity

added theorem multiplicity.pow_multiplicity_dvd

added theorem multiplicity.unique'

added theorem multiplicity.unique

added theorem multiplicity.unit_left

added theorem multiplicity.unit_right

added def multiplicity

added theorem multiplicity_eq_zero_of_coprime