Basic

📁 Source: Mathlib/Data/Nat/Factorization/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems Icc_factorization_eq_pow_dvd, Ico_filter_pow_dvd_eq, Ico_pow_dvd_eq_Ico_of_lt, Ioc_filter_dvd_card_eq_div, dvd_iff_one_le_factorization, eq_of_factorization_pos, factorization_self, pow_dvd_iff_dvd_ordProj, pow_dvd_iff_le_factorization, card_multiples, card_multiples', coprime_ordCompl, dvd_iff_div_factorization_eq_tsub, dvd_iff_prime_pow_dvd_dvd, dvd_of_factorization_pos, dvd_ordCompl_of_dvd_not_dvd, dvd_ordProj_of_dvd, eq_factorization_iff, eq_iff_prime_padicValNat_eq, eq_pow_of_factorization_eq_single, exists_eq_pow_mul_and_not_dvd, exists_eq_pow_of_exponent_coprime_of_pow_eq_pow, exists_eq_pow_of_pow_eq_pow, exists_eq_two_pow_mul_odd, exists_factorization_lt_of_lt, factorizationEquiv_inv_apply, factorization_div, factorization_eq_card_pow_dvd, factorization_eq_card_pow_dvd_of_lt, factorization_eq_of_coprime_left, factorization_eq_of_coprime_right, factorization_eq_zero_iff', factorization_eq_zero_iff_remainder, factorization_eq_zero_of_lt, factorization_gcd, factorization_lcm, factorization_le_factorization_mul_left, factorization_le_factorization_mul_right, factorization_le_of_le_pow, factorization_lt, factorization_ordCompl, factorization_pow_self, factorization_prime_le_iff_dvd, factorization_prod_apply, not_dvd_ordCompl, ordCompl_dvd, ordCompl_dvd_ordCompl_iff_dvd, ordCompl_dvd_ordCompl_of_dvd, ordCompl_eq_self_iff_zero_or_not_dvd, ordCompl_le, ordCompl_mul, ordCompl_of_not_prime, ordCompl_pos, ordCompl_self_pow, ordCompl_self_pow_mul, ordProj_dvd_ordProj_of_dvd, ordProj_le, ordProj_mul, ordProj_mul_ordCompl_eq_self, ordProj_of_not_prime, ordProj_pos, ordProj_self_pow, pairwise_coprime_pow_primeFactors_factorization, prod_factorization_eq_prod_primeFactors, prod_pow_primeFactors_factorization, prod_pow_prime_padicValNat, prod_primeFactors_dvd, prod_primeFactors_gcd_mul_prod_primeFactors_mul, prod_primeFactors_prod_factorization, setOf_pow_dvd_eq_Icc_factorization, sum_primeFactors_gcd_add_sum_primeFactors_mul	71
Total	71

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Icc_factorization_eq_pow_dvd 📖	mathematical	Prime	Finset.Icc instPreorder instLocallyFiniteOrder DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization Finset.filter Monoid.toNatPow instMonoid Finset.Ico	—	eq_or_ne factorization_zero Finset.Icc_eq_empty_of_lt instZeroLEOneClass Finset.filter.congr_simp Finset.Ico_eq_empty_of_le instCanonicallyOrderedAdd Finset.filter_empty Finset.ext Prime.pow_dvd_iff_le_factorization lt_of_le_of_lt factorization_lt
Ico_filter_pow_dvd_eq 📖	mathematical	Prime Monoid.toNatPow instMonoid	Finset.filter Finset.Ico instPreorder instLocallyFiniteOrder Finset.Icc	—	Finset.ext Prime.two_le Prime.one_lt LE.le.trans Ne.bot_lt
Ico_pow_dvd_eq_Ico_of_lt 📖	mathematical	Prime Monoid.toNatPow instMonoid	Finset.filter Finset.Ico instPreorder instLocallyFiniteOrder	—	Finset.ext zero_dvd_iff zero_pow Prime.one_lt lt_of_le_of_lt
Ioc_filter_dvd_card_eq_div 📖	mathematical	—	Finset.card Finset.filter Finset.Ioc instPreorder instLocallyFiniteOrder	—	Finset.filter.congr_simp Finset.Ioc_eq_empty_of_le Finset.filter_empty instNoMaxOrder instCanonicallyOrderedAdd Finset.filter_insert Finset.card_insert_of_notMem IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le add_ite add_zero
card_multiples 📖	mathematical	—	Finset.card Finset.filter Finset.range	—	Finset.filter_empty Finset.filter.congr_simp Finset.range_add_one Finset.filter_insert Finset.card_insert_of_notMem add_ite add_zero
card_multiples' 📖	mathematical	—	Finset.card Finset.filter Finset.range	—	Finset.filter.congr_simp zero_add Finset.filter_false_of_mem Finset.range_add_one Finset.filter_insert Finset.card_insert_of_notMem
coprime_ordCompl 📖	mathematical	Prime	Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	not_dvd_ordCompl coprime_or_dvd_of_prime
dvd_iff_div_factorization_eq_tsub 📖	mathematical	—	factorization Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.tsub instAddCommMonoid instPartialOrder instCanonicallyOrderedAdd instOrderedSub	—	instCanonicallyOrderedAdd instOrderedSub factorization_div eq_or_lt_of_le tsub_self Finsupp.instCanonicallyOrderedAddOfAddLeftMono IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Finsupp.orderedSub exists_factorization_lt_of_lt mul_ne_zero IsStrictOrderedRing.noZeroDivisors instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE not_le lt_self_iff_false Finsupp.tsub_apply lt_tsub_iff_right Finsupp.add_apply factorization_mul
dvd_iff_prime_pow_dvd_dvd 📖	mathematical	—	Monoid.toNatPow instMonoid	—	eq_or_ne prime_two dvd_zero Ne.bot_lt LT.lt.not_ge dvd_trans factorization_prime_le_iff_dvd Prime.pow_dvd_iff_le_factorization ordProj_dvd
dvd_of_factorization_pos 📖	—	—	—	—	dvd_of_mem_primeFactorsList mem_primeFactors_iff_mem_primeFactorsList Finsupp.mem_support_iff
dvd_ordCompl_of_dvd_not_dvd 📖	mathematical	—	Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	factorization_zero pow_zero factorization_le_iff_dvd LT.lt.ne' ordCompl_pos factorization_ordCompl Finsupp.erase_same instCanonicallyOrderedAdd Finsupp.erase_ne
dvd_ordProj_of_dvd 📖	mathematical	Prime	Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	dvd_pow_self LT.lt.ne' Prime.factorization_pos_of_dvd
eq_factorization_iff 📖	mathematical	Prime	factorization Finsupp.prod MulZeroClass.toZero instMulZeroClass instCommMonoid Monoid.toNatPow instMonoid	—	factorization_prod_pow_eq_self prod_pow_factorization_eq_self
eq_iff_prime_padicValNat_eq 📖	mathematical	—	padicValNat	—	eq_of_factorization_eq factorization_def factorization_eq_zero_of_not_prime
eq_pow_of_factorization_eq_single 📖	mathematical	factorization Finsupp.single MulZeroClass.toZero instMulZeroClass	Monoid.toNatPow instMonoid	—	factorization_prod_pow_eq_self Finsupp.prod_single_index pow_zero
exists_eq_pow_mul_and_not_dvd 📖	mathematical	—	Monoid.toNatPow instMonoid	—	FiniteMultiplicity.exists_eq_pow_mul_and_not_dvd finiteMultiplicity_iff
exists_eq_pow_of_exponent_coprime_of_pow_eq_pow 📖	—	Monoid.toNatPow instMonoid	—	—	pow_one pow_zero zero_pow eq_of_factorization_eq instNontrivial IsStrictOrderedRing.noZeroDivisors instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE instCanonicallyOrderedAdd factorization_zero_right prime_of_mem_primeFactors Finsupp.support_mapRange factorization_pow prod_pow_factorization_eq_self pow_left_injective
exists_eq_pow_of_pow_eq_pow 📖	—	Monoid.toNatPow instMonoid	—	—	pow_left_injective pow_mul exists_eq_pow_of_exponent_coprime_of_pow_eq_pow
exists_eq_two_pow_mul_odd 📖	mathematical	—	Odd instSemiring Monoid.toNatPow instMonoid	—	exists_eq_pow_mul_and_not_dvd not_even_iff_odd instAtLeastTwoHAddOfNat Even.two_dvd
exists_factorization_lt_of_lt 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	LT.lt.ne' LT.lt.trans Ne.bot_lt Mathlib.Tactic.Contrapose.contrapose₁ factorization_le_iff_dvd Finsupp.le_def
factorizationEquiv_inv_apply 📖	mathematical	Prime	DFunLike.coe Equiv Set.Elem Finsupp MulZeroClass.toZero instMulZeroClass setOf PNat EquivLike.toFunLike Equiv.instEquivLike Equiv.symm factorizationEquiv Set Set.instMembership Finsupp.prod instCommMonoid Monoid.toNatPow instMonoid	—	—
factorization_div 📖	mathematical	—	factorization Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.tsub instAddCommMonoid instPartialOrder instCanonicallyOrderedAdd instOrderedSub	—	instCanonicallyOrderedAdd instOrderedSub eq_or_ne zero_dvd_iff factorization_zero tsub_self Finsupp.instCanonicallyOrderedAddOfAddLeftMono IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Finsupp.orderedSub tsub_eq_zero_of_le add_left_injective Finsupp.instIsRightCancelAdd AddRightCancelSemigroup.toIsRightCancelAdd tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Finsupp.isOrderedAddMonoid factorization_le_iff_dvd factorization_mul LT.lt.ne' Ne.bot_lt
factorization_eq_card_pow_dvd 📖	mathematical	Prime	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization Finset.card Finset.filter Monoid.toNatPow instMonoid Finset.Ico instPreorder instLocallyFiniteOrder	—	Icc_factorization_eq_pow_dvd card_Icc add_tsub_cancel_right instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
factorization_eq_card_pow_dvd_of_lt 📖	mathematical	Prime Monoid.toNatPow instMonoid	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization Finset.card Finset.filter Finset.Ico instPreorder instLocallyFiniteOrder	—	factorization_eq_card_pow_dvd Ico_pow_dvd_eq_Ico_of_lt
factorization_eq_of_coprime_left 📖	mathematical	primeFactorsList	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	factorization_mul_apply_of_coprime primeFactorsList_count_eq coprime_primeFactorsList_disjoint add_zero
factorization_eq_of_coprime_right 📖	mathematical	primeFactorsList	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	mul_comm factorization_eq_of_coprime_left
factorization_eq_zero_iff' 📖	mathematical	—	factorization Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instZero	—	factorization_eq_primeFactorsList_multiset EquivLike.toEmbeddingLike AddMonoidHomClass.toZeroHomClass AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
factorization_eq_zero_iff_remainder 📖	mathematical	Prime	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	factorization_eq_zero_of_remainder Mathlib.Tactic.Contrapose.contrapose₃ dvd_mul_right Mathlib.Tactic.Contrapose.contrapose₄ add_eq_zero Unique.instSubsingleton factorization_eq_zero_iff
factorization_eq_zero_of_lt 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	Finsupp.notMem_support_iff le_of_mem_primeFactors not_le_of_gt
factorization_gcd 📖	mathematical	—	factorization Finsupp MulZeroClass.toZero instMulZeroClass SemilatticeInf.toMin Finsupp.semilatticeInf Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeNat	—	Finsupp.support_inf instCanonicallyOrderedAdd prime_of_mem_primeFactorsList prod_pow_factorization_eq_self LT.lt.ne' gcd_greatest factorization_le_iff_dvd inf_le_left inf_le_right Decidable.eq_or_ne
factorization_lcm 📖	mathematical	—	factorization Finsupp MulZeroClass.toZero instMulZeroClass SemilatticeSup.toMax Finsupp.semilatticeSup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeNat	—	Finsupp.instIsLeftCancelAdd AddLeftCancelSemigroup.toIsLeftCancelAdd factorization_mul factorization_gcd Finsupp.ext min_add_max
factorization_le_factorization_mul_left 📖	mathematical	—	Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instLE factorization	—	eq_or_ne factorization_zero MulZeroClass.zero_mul factorization_le_iff_dvd mul_ne_zero IsStrictOrderedRing.noZeroDivisors instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE instCanonicallyOrderedAdd Dvd.intro
factorization_le_factorization_mul_right 📖	mathematical	—	Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instLE factorization	—	mul_comm factorization_le_factorization_mul_left
factorization_le_of_le_pow 📖	mathematical	Monoid.toNatPow instMonoid	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	factorization_zero instCanonicallyOrderedAdd Prime.one_lt LE.le.trans ordProj_le factorization_eq_zero_of_not_prime
factorization_lt 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	Prime.one_lt LE.le.trans_lt ordProj_le factorization_eq_zero_of_not_prime Ne.bot_lt
factorization_ordCompl 📖	mathematical	—	factorization Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike Finsupp.erase	—	factorization_zero pow_zero Finsupp.erase_of_notMem_support Finsupp.ext eq_or_ne Finsupp.erase_same not_dvd_ordCompl Finsupp.erase_ne instCanonicallyOrderedAdd instOrderedSub factorization_div ordProj_dvd factorization_pow Prime.factorization Finsupp.smul_single mul_one Finsupp.single_eq_of_ne' tsub_zero factorization_eq_zero_of_not_prime
factorization_pow_self 📖	mathematical	Prime	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization Monoid.toNatPow instMonoid	—	factorization_pow Prime.factorization_self mul_one
factorization_prime_le_iff_dvd 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	factorization_le_iff_dvd em factorization_eq_zero_of_not_prime le_refl
factorization_prod_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization Finset.prod instCommMonoid Finset.sum instAddCommMonoid	—	factorization_prod Finsupp.finset_sum_apply
not_dvd_ordCompl 📖	mathematical	Prime	Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	Prime.dvd_iff_one_le_factorization LT.lt.ne' ordCompl_pos instCanonicallyOrderedAdd instOrderedSub factorization_div ordProj_dvd factorization_pow Prime.factorization Finsupp.smul_single mul_one Finsupp.single_eq_same tsub_self
ordCompl_dvd 📖	mathematical	—	Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	ordProj_dvd
ordCompl_dvd_ordCompl_iff_dvd 📖	mathematical	—	Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	eq_or_ne prime_dvd_prime_iff_eq Prime.ne_one Ne.bot_lt mul_one Prime.factorization Finsupp.single_eq_of_ne' pow_zero Prime.factorization_self pow_one factorization_eq_zero_of_not_prime ordCompl_dvd_ordCompl_of_dvd
ordCompl_dvd_ordCompl_of_dvd 📖	mathematical	—	Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	em' factorization_eq_zero_of_not_prime pow_zero eq_or_ne factorization_zero zero_dvd_iff LT.lt.ne' ordProj_le ordProj_pos factorization_le_iff_dvd factorization_ordCompl Finsupp.erase_same Finsupp.erase_ne
ordCompl_eq_self_iff_zero_or_not_dvd 📖	mathematical	Prime	Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	not_dvd_ordCompl factorization_zero pow_zero factorization_eq_zero_of_not_dvd
ordCompl_le 📖	mathematical	—	Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	—
ordCompl_mul 📖	mathematical	—	Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	MulZeroClass.zero_mul factorization_zero pow_zero MulZeroClass.mul_zero ordProj_mul ordProj_dvd
ordCompl_of_not_prime 📖	mathematical	Prime	Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	factorization_eq_zero_of_not_prime pow_zero
ordCompl_pos 📖	mathematical	—	Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	ordProj_le ordProj_pos factorization_eq_zero_of_not_prime pow_zero Ne.bot_lt
ordCompl_self_pow 📖	mathematical	Prime	Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	eq_of_factorization_eq pos_iff_ne_zero instCanonicallyOrderedAdd ordCompl_pos pow_ne_zero isReduced_of_noZeroDivisors IsStrictOrderedRing.noZeroDivisors instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Prime.ne_zero one_ne_zero instOrderedSub Prime.factorization_pow Finsupp.single_eq_same factorization_div tsub_self Finsupp.instCanonicallyOrderedAddOfAddLeftMono IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Finsupp.orderedSub factorization_one
ordCompl_self_pow_mul 📖	mathematical	Prime	Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	ordCompl_mul ordCompl_self_pow one_mul
ordProj_dvd_ordProj_of_dvd 📖	mathematical	—	Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	em' factorization_eq_zero_of_not_prime pow_zero eq_or_ne factorization_zero Unique.instSubsingleton Prime.one_lt factorization_le_iff_dvd
ordProj_le 📖	mathematical	—	Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	Ne.bot_lt ordProj_dvd
ordProj_mul 📖	mathematical	—	Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	factorization_mul pow_add
ordProj_mul_ordCompl_eq_self 📖	mathematical	—	Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	ordProj_dvd
ordProj_of_not_prime 📖	mathematical	Prime	Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	factorization_eq_zero_of_not_prime pow_zero
ordProj_pos 📖	mathematical	—	Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	Prime.pos factorization_eq_zero_of_not_prime pow_zero instZeroLEOneClass
ordProj_self_pow 📖	mathematical	Prime	Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	factorization_pow Prime.factorization Finsupp.smul_single mul_one Finsupp.single_eq_same
pairwise_coprime_pow_primeFactors_factorization 📖	mathematical	—	Pairwise Finset SetLike.instMembership Finset.instSetLike primeFactors Function.onFun Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	coprime_primes prime_of_mem_primeFactors Subtype.coe_ne_coe
prod_factorization_eq_prod_primeFactors 📖	mathematical	—	Finsupp.prod MulZeroClass.toZero instMulZeroClass factorization Finset.prod primeFactors DFunLike.coe Finsupp Finsupp.instFunLike	—	—
prod_pow_primeFactors_factorization 📖	mathematical	—	Finset.prod Finset SetLike.instMembership Finset.instSetLike primeFactors instCommMonoid Finset.univ Finset.Subtype.fintype Monoid.toNatPow instMonoid DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	factorization_prod_pow_eq_self prod_factorization_eq_prod_primeFactors Finset.prod_subtype
prod_pow_prime_padicValNat 📖	mathematical	—	Finset.prod instCommMonoid Finset.filter Prime decidablePrime Finset.range Monoid.toNatPow instMonoid padicValNat	—	factorization_prod_pow_eq_self Finset.prod_subset_one_on_sdiff Finset.mem_filter Finset.mem_range LT.lt.trans_le' le_of_mem_primeFactors prime_of_mem_primeFactors Finset.mem_sdiff factorization_def Finsupp.notMem_support_iff pow_zero
prod_primeFactors_dvd 📖	mathematical	—	Finset.prod instCommMonoid primeFactors	—	Finset.prod_congr primeFactors_zero Unique.instSubsingleton prod_primeFactorsList Multiset.toFinset_prod_dvd_prod
prod_primeFactors_gcd_mul_prod_primeFactors_mul 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Finset.prod primeFactors	—	eq_or_ne Finset.prod_congr MulZeroClass.zero_mul primeFactors_zero mul_one one_mul MulZeroClass.mul_zero primeFactors_mul primeFactors_gcd mul_comm Finset.prod_union_inter
prod_primeFactors_prod_factorization 📖	mathematical	—	Finset.prod primeFactors Finsupp.prod MulZeroClass.toZero instMulZeroClass factorization	—	—
setOf_pow_dvd_eq_Icc_factorization 📖	mathematical	Prime	setOf Monoid.toNatPow instMonoid Set.Icc instPreorder DFunLike.coe Finsupp MulZeroClass.toZero instMulZeroClass Finsupp.instFunLike factorization	—	Set.ext Prime.pow_dvd_iff_le_factorization
sum_primeFactors_gcd_add_sum_primeFactors_mul 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finset.sum primeFactors	—	eq_or_ne Finset.sum_congr MulZeroClass.zero_mul primeFactors_zero add_zero zero_add MulZeroClass.mul_zero primeFactors_mul primeFactors_gcd add_comm Finset.sum_union_inter

Nat.Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dvd_iff_one_le_factorization 📖	mathematical	Nat.Prime	DFunLike.coe Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instFunLike Nat.factorization	—	pow_one pow_dvd_iff_le_factorization
eq_of_factorization_pos 📖	—	Nat.Prime	—	—	factorization Finsupp.single_apply
factorization_self 📖	mathematical	Nat.Prime	DFunLike.coe Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instFunLike Nat.factorization	—	factorization Finsupp.single_eq_same
pow_dvd_iff_dvd_ordProj 📖	mathematical	Nat.Prime	Monoid.toNatPow Nat.instMonoid DFunLike.coe Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instFunLike Nat.factorization	—	one_lt pow_dvd_iff_le_factorization
pow_dvd_iff_le_factorization 📖	mathematical	Nat.Prime	Monoid.toNatPow Nat.instMonoid DFunLike.coe Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instFunLike Nat.factorization	—	Nat.factorization_le_iff_dvd LT.lt.ne' pos factorization_pow Finsupp.single_le_iff Nat.instCanonicallyOrderedAdd

---

← Back to Index