Multiplicity

📁 Source: Mathlib/Data/Nat/Multiplicity.lean

Statistics

Metric	Count
Definitions	0
Theorems dvd_choose_pow, dvd_choose_pow_iff, emultiplicity_choose, emultiplicity_choose', emultiplicity_choose_prime_pow, emultiplicity_choose_prime_pow_add_emultiplicity, emultiplicity_factorial, emultiplicity_factorial_le_div_pred, emultiplicity_factorial_mul, emultiplicity_factorial_mul_succ, emultiplicity_le_emultiplicity_choose_add, emultiplicity_mul, emultiplicity_one, emultiplicity_pow, emultiplicity_pow_self, emultiplicity_self, multiplicity_factorial_pow, pow_dvd_factorial_iff, sub_one_mul_multiplicity_factorial, emultiplicity_eq_card_pow_dvd, emultiplicity_two_factorial_lt	21
Total	21

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
emultiplicity_eq_card_pow_dvd 📖	mathematical	log	emultiplicity instMonoid ENat ENat.instNatCast Finset.card Finset.filter Monoid.toNatPow Finset.Ico instPreorder instLocallyFiniteOrder	—	finiteMultiplicity_iff FiniteMultiplicity.emultiplicity_eq_multiplicity card_Ico add_tsub_cancel_right instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Finset.ext Finset.filter.congr_simp FiniteMultiplicity.pow_dvd_iff_le_multiplicity LT.lt.ne' zero_dvd_iff zero_pow LE.le.trans_lt le_log_of_pow_le
emultiplicity_two_factorial_lt 📖	mathematical	—	ENat Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat emultiplicity instMonoid factorial ENat.instNatCast	—	Prime.prime prime_two MulZeroClass.mul_zero zero_add Prime.emultiplicity_one zero_lt_one IsOrderedRing.toZeroLEOneClass NeZero.charZero_one Prime.emultiplicity_factorial_mul instAtLeastTwoHAddOfNat two_mul cast_add WithTop.add_lt_add_right IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid cast_mul emultiplicity_eq_zero two_not_dvd_two_mul_add_one LT.lt.trans cast_one LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid emultiplicity_mul instIsCancelMulZero

Nat.Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dvd_choose_pow 📖	mathematical	Nat.Prime	Nat.choose Monoid.toNatPow Nat.instMonoid	—	Ne.lt_or_gt Nat.choose_eq_zero_of_lt emultiplicity_ne_zero LT.lt.not_ge Ne.bot_lt emultiplicity_choose_prime_pow_add_emultiplicity LT.lt.le emultiplicity_eq_coe zero_add
dvd_choose_pow_iff 📖	mathematical	Nat.Prime	Nat.choose Monoid.toNatPow Nat.instMonoid	—	Nat.choose_zero_right ne_one Nat.choose_self dvd_choose_pow
emultiplicity_choose 📖	mathematical	Nat.Prime Nat.log	emultiplicity Nat.instMonoid Nat.choose ENat ENat.instNatCast Finset.card Finset.filter Monoid.toNatPow Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder	—	emultiplicity_choose'
emultiplicity_choose' 📖	mathematical	Nat.Prime Nat.log	emultiplicity Nat.instMonoid Nat.choose ENat ENat.instNatCast Finset.card Finset.filter Monoid.toNatPow Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder	—	emultiplicity_mul mul_assoc Nat.choose_mul_factorial_mul_factorial add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid emultiplicity_factorial LE.le.trans_lt Nat.log_mono_right add_comm Nat.multiplicity_choose_aux Finset.sum_congr Finset.filter.congr_simp Nat.cast_add Nat.cast_sum WithTop.add_right_cancel AddRightCancelSemigroup.toIsRightCancelAdd finiteMultiplicity_iff_emultiplicity_ne_top Nat.finiteMultiplicity_iff ne_one mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.factorial_pos
emultiplicity_choose_prime_pow 📖	mathematical	Nat.Prime Monoid.toNatPow Nat.instMonoid	emultiplicity Nat.choose ENat ENat.instNatCast multiplicity	—	emultiplicity_choose_prime_pow_add_emultiplicity FiniteMultiplicity.emultiplicity_eq_multiplicity Nat.finiteMultiplicity_iff ne_one Nat.choose_pos
emultiplicity_choose_prime_pow_add_emultiplicity 📖	mathematical	Nat.Prime Monoid.toNatPow Nat.instMonoid	ENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat emultiplicity Nat.choose ENat.instNatCast	—	le_antisymm Finset.filter.congr_simp Nat.instNoMaxOrder zero_add pow_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.instZeroLEOneClass pos emultiplicity_choose Nat.emultiplicity_eq_card_pow_dvd one_lt Ne.bot_lt Nat.log_mono_right Nat.cast_add WithTop.coe_mono Nat.log_pow Finset.card_union_of_disjoint Finset.filter_union_right Finset.card_filter_le Nat.card_Ico emultiplicity_pow_self emultiplicity_le_emultiplicity_choose_add
emultiplicity_factorial 📖	mathematical	Nat.Prime Nat.log	emultiplicity Nat.instMonoid Nat.factorial ENat ENat.instNatCast Finset.sum Nat.instAddCommMonoid Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder Monoid.toNatPow	—	emultiplicity_one Finset.sum_congr Finset.sum_const_zero Nat.cast_zero Nat.factorial_succ emultiplicity_mul add_comm LE.le.trans_lt Nat.log_mono_right Nat.emultiplicity_eq_card_pow_dvd ne_one Finset.sum_add_distrib Finset.sum_boole Nat.cast_sum Nat.cast_add
emultiplicity_factorial_le_div_pred 📖	mathematical	Nat.Prime	ENat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat emultiplicity Nat.instMonoid Nat.factorial ENat.instNatCast	—	emultiplicity_factorial WithTop.coe_mono Nat.geom_sum_Ico_le two_le
emultiplicity_factorial_mul 📖	mathematical	Nat.Prime	emultiplicity Nat.instMonoid Nat.factorial ENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat ENat.instNatCast	—	MulZeroClass.mul_zero Nat.cast_zero add_zero emultiplicity_factorial_mul_succ emultiplicity_mul Nat.cast_add Nat.cast_one add_comm add_assoc
emultiplicity_factorial_mul_succ 📖	mathematical	Nat.Prime	emultiplicity Nat.instMonoid Nat.factorial ENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	prime two_le le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing Mathlib.Tactic.Linarith.mul_neg neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Meta.NormNum.isNat_lt_true IsStrictOrderedRing.toIsOrderedRing Int.instCharZero Mathlib.Tactic.Linarith.sub_nonpos_of_le Nat.cast_mul Nat.cast_add Nat.cast_one emultiplicity_eq_top Nat.finiteMultiplicity_iff ne_one Nat.factorial_pos Finset.emultiplicity_prod Nat.instIsCancelMulZero Finset.sum_Ico_consecutive add_assoc AddLeftCancelSemigroup.toIsLeftCancelAdd Finset.sum_Ico_succ_top emultiplicity_mul emultiplicity_self Finset.sum_congr emultiplicity_eq_zero pos Finset.mem_Ico Finset.sum_const_zero zero_add add_comm
emultiplicity_le_emultiplicity_choose_add 📖	mathematical	Nat.Prime	ENat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat emultiplicity Nat.instMonoid Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.choose	—	Nat.choose_zero_right emultiplicity_zero add_top top_add emultiplicity_mul emultiplicity_le_emultiplicity_of_dvd_right Nat.add_one_mul_choose_eq dvd_mul_right
emultiplicity_mul 📖	mathematical	Nat.Prime	emultiplicity Nat.instMonoid ENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	emultiplicity_mul Nat.instIsCancelMulZero prime
emultiplicity_one 📖	mathematical	Nat.Prime	emultiplicity Nat.instMonoid ENat instZeroENat	—	emultiplicity_of_one_right Prime.not_unit prime
emultiplicity_pow 📖	mathematical	Nat.Prime	emultiplicity Nat.instMonoid Monoid.toNatPow ENat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat ENat.instNatCast	—	emultiplicity_pow Nat.instIsCancelMulZero prime
emultiplicity_pow_self 📖	mathematical	Nat.Prime	emultiplicity Nat.instMonoid Monoid.toNatPow ENat ENat.instNatCast	—	emultiplicity_pow_self Nat.instIsCancelMulZero ne_zero Prime.not_unit prime
emultiplicity_self 📖	mathematical	Nat.Prime	emultiplicity Nat.instMonoid ENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	FiniteMultiplicity.emultiplicity_self Nat.instIsCancelMulZero Nat.finiteMultiplicity_iff ne_one pos
multiplicity_factorial_pow 📖	mathematical	Nat.Prime	multiplicity Nat.instMonoid Nat.factorial Monoid.toNatPow Finset.sum Nat.instAddCommMonoid Finset.range	—	FiniteMultiplicity.emultiplicity_eq_multiplicity Nat.finiteMultiplicity_iff ne_one Nat.factorial_pos pow_zero emultiplicity_one Nat.cast_zero emultiplicity_factorial_mul Finset.sum_range_succ ENat.coe_add
pow_dvd_factorial_iff 📖	mathematical	Nat.Prime Nat.log	Monoid.toNatPow Nat.instMonoid Nat.factorial Finset.sum Nat.instAddCommMonoid Finset.Ico Nat.instPreorder Nat.instLocallyFiniteOrder	—	WithTop.coe_le_coe ENat.some_eq_coe emultiplicity_factorial pow_dvd_iff_le_emultiplicity
sub_one_mul_multiplicity_factorial 📖	mathematical	Nat.Prime	multiplicity Nat.instMonoid Nat.factorial MulZeroClass.toZero Nat.instMulZeroClass Nat.digits	—	multiplicity_eq_of_emultiplicity_eq_some emultiplicity_factorial Finset.sum_Ico_add' Nat.instIsOrderedCancelAddMonoid CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd Finset.sum_congr Nat.Ico_zero_eq_range

---

← Back to Index