Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-05 14:19 b9c5eb05

View on Github →

feat(ring_theory/multiplicity): multiplicity of elements of a ring (#523)

Estimated changes

Modified algebra/group_power.lean

added theorem pow_dvd_pow

Modified data/multiset.lean

added theorem multiset.card_smul

Modified data/nat/basic.lean

Modified data/rat.lean

added theorem rat.add_num_denom

added theorem rat.denom_one

added theorem rat.num_one

Created ring_theory/multiplicity.lean

added theorem multiplicity.dvd_of_multiplicity_pos

added theorem multiplicity.eq_some_iff

added theorem multiplicity.eq_top_iff

added theorem multiplicity.eq_top_iff_not_finite

added def multiplicity.finite

added theorem multiplicity.finite_def

added theorem multiplicity.finite_iff_dom

added theorem multiplicity.finite_int_iff

added theorem multiplicity.finite_int_iff_nat_abs_finite

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.is_greatest'

added theorem multiplicity.is_greatest

added theorem multiplicity.le_multiplicity_of_pow_dvd

added theorem multiplicity.min_le_multiplicity_add

added theorem multiplicity.multiplicity_eq_zero_of_not_dvd

added theorem multiplicity.multiplicity_le_multiplicity_iff

added theorem multiplicity.multiplicity_self

added theorem multiplicity.multiplicity_unit

added theorem multiplicity.ne_zero_of_finite

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.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 def multiplicity

added theorem multiplicity_eq_zero_of_coprime