Factors

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

Statistics

Metric	Count
Definitions primeFactorsList	1
Theorems primeFactorsList_pow, coprime_primeFactorsList_disjoint, dvd_of_mem_primeFactorsList, dvd_of_primeFactorsList_subperm, eq_of_perm_primeFactorsList, eq_prime_pow_of_unique_prime_dvd, eq_two_pow_or_exists_odd_prime_and_dvd, four_dvd_or_exists_odd_prime_and_dvd_of_two_lt, isChain_cons_primeFactorsList, isChain_primeFactorsList, isChain_two_cons_primeFactorsList, le_of_mem_primeFactorsList, mem_primeFactorsList, mem_primeFactorsList', mem_primeFactorsList_iff_dvd, mem_primeFactorsList_mul, mem_primeFactorsList_mul_left, mem_primeFactorsList_mul_of_coprime, mem_primeFactorsList_mul_right, perm_primeFactorsList_mul, perm_primeFactorsList_mul_of_coprime, pos_of_mem_primeFactorsList, primeFactorsList_add_two, primeFactorsList_chain, primeFactorsList_chain', primeFactorsList_chain_2, primeFactorsList_eq_nil, primeFactorsList_ne_nil, primeFactorsList_one, primeFactorsList_prime, primeFactorsList_sorted, primeFactorsList_sublist_of_dvd, primeFactorsList_sublist_right, primeFactorsList_subset_of_dvd, primeFactorsList_subset_right, primeFactorsList_two, primeFactorsList_unique, primeFactorsList_zero, prime_of_mem_primeFactorsList, prod_primeFactorsList, replicate_subperm_primeFactorsList_iff	41
Total	42

Nat

Definitions

Name	Category	Theorems
primeFactorsList 📖	CompOp	45 math math: mem_primeFactorsList_iff_dvd, primeFactorsList_sorted, prod_mem_smoothNumbers, perm_primeFactorsList_mul_of_coprime, ArithmeticFunction.cardDistinctFactors_apply, isChain_primeFactorsList, prod_mem_factoredNumbers, ArithmeticFunction.cardFactors_apply, isChain_two_cons_primeFactorsList, Mathlib.Meta.Simproc.FactorsHelper.primeFactorsList_eq, Prime.primeFactorsList_pow, primeFactorsList_add_two, primeFactorsList_chain_2, primeFactorsList_prime, primeFactorsList_sublist_right, primeFactorsList_unique, factors_eq, primeFactorsList_two, isChain_cons_primeFactorsList, toFinset_factors, primeFactorsList_count_eq, mem_primeFactorsList, primeFactorsList_subset_of_dvd, le_padicValNat_iff_replicate_subperm_primeFactorsList, primeFactorsList_chain', primeFactorsList_one, squarefree_iff_nodup_primeFactorsList, primeFactorsList_chain, factorization_eq_primeFactorsList_multiset, Squarefree.nodup_primeFactorsList, perm_primeFactorsList_mul, mem_primeFactors_iff_mem_primeFactorsList, primeFactorsList_subset_right, mem_primeFactorsList', PNat.coeNat_factorMultiset, mem_primeFactorsList_mul_of_coprime, mem_primeFactorsList_mul, eq_prime_pow_of_unique_prime_dvd, replicate_subperm_primeFactorsList_iff, le_emultiplicity_iff_replicate_subperm_primeFactorsList, primeFactorsList_eq_nil, coprime_primeFactorsList_disjoint, prod_primeFactorsList, primeFactorsList_zero, primeFactorsList_sublist_of_dvd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coprime_primeFactorsList_disjoint 📖	mathematical	—	primeFactorsList	—	not_prime_one eq_one_of_dvd_coprimes dvd_of_mem_primeFactorsList prime_of_mem_primeFactorsList
dvd_of_mem_primeFactorsList 📖	—	primeFactorsList	—	—	dvd_zero mem_primeFactorsList_iff_dvd LT.lt.ne' prime_of_mem_primeFactorsList
dvd_of_primeFactorsList_subperm 📖	—	primeFactorsList	—	—	dvd_zero one_dvd prod_primeFactorsList List.Perm.prod_eq LT.lt.ne'
eq_of_perm_primeFactorsList 📖	—	primeFactorsList	—	—	prod_primeFactorsList List.Perm.prod_eq
eq_prime_pow_of_unique_prime_dvd 📖	mathematical	—	Monoid.toNatPow instMonoid primeFactorsList	—	prod_primeFactorsList List.prod_replicate prime_of_mem_primeFactorsList dvd_of_mem_primeFactorsList
eq_two_pow_or_exists_odd_prime_and_dvd 📖	mathematical	—	Monoid.toNatPow instMonoid Prime Odd instSemiring	—	eq_or_ne prime_three dvd_zero eq_prime_pow_of_unique_prime_dvd Prime.eq_two_or_odd'
four_dvd_or_exists_odd_prime_and_dvd_of_two_lt 📖	mathematical	—	Prime Odd instSemiring	—	eq_two_pow_or_exists_odd_prime_and_dvd mul_assoc
isChain_cons_primeFactorsList 📖	mathematical	—	primeFactorsList	—	primeFactorsList_zero primeFactorsList_one factors_lemma primeFactorsList.eq_3 le_minFac minFac_le_of_dvd Prime.two_le Dvd.dvd.trans minFac_dvd
isChain_primeFactorsList 📖	mathematical	—	primeFactorsList	—	List.IsChain.tail isChain_two_cons_primeFactorsList
isChain_two_cons_primeFactorsList 📖	mathematical	—	primeFactorsList	—	isChain_cons_primeFactorsList Prime.two_le
le_of_mem_primeFactorsList 📖	—	primeFactorsList	—	—	primeFactorsList_zero dvd_of_mem_primeFactorsList
mem_primeFactorsList 📖	mathematical	—	primeFactorsList Prime	—	prime_of_mem_primeFactorsList dvd_of_mem_primeFactorsList mem_primeFactorsList_iff_dvd
mem_primeFactorsList' 📖	mathematical	—	primeFactorsList Prime	—	primeFactorsList_zero
mem_primeFactorsList_iff_dvd 📖	mathematical	Prime	primeFactorsList	—	List.dvd_prod prod_primeFactorsList mem_list_primes_of_dvd_prod instIsCancelMulZero Unique.instSubsingleton prime_iff prime_of_mem_primeFactorsList
mem_primeFactorsList_mul 📖	mathematical	—	primeFactorsList	—	mem_primeFactorsList mul_ne_zero IsDomain.to_noZeroDivisors instIsDomain Prime.dvd_mul
mem_primeFactorsList_mul_left 📖	—	primeFactorsList	—	—	eq_or_ne primeFactorsList_zero mem_primeFactorsList_mul
mem_primeFactorsList_mul_of_coprime 📖	mathematical	—	primeFactorsList	—	mul_one primeFactorsList_zero primeFactorsList_one MulZeroClass.mul_zero mem_primeFactorsList_mul LT.lt.ne'
mem_primeFactorsList_mul_right 📖	—	primeFactorsList	—	—	mul_comm mem_primeFactorsList_mul_left
perm_primeFactorsList_mul 📖	mathematical	—	primeFactorsList	—	primeFactorsList_unique prod_primeFactorsList prime_of_mem_primeFactorsList
perm_primeFactorsList_mul_of_coprime 📖	mathematical	—	primeFactorsList	—	mul_one primeFactorsList_zero primeFactorsList_one MulZeroClass.mul_zero perm_primeFactorsList_mul LT.lt.ne'
pos_of_mem_primeFactorsList 📖	—	primeFactorsList	—	—	Prime.pos prime_of_mem_primeFactorsList
primeFactorsList_add_two 📖	mathematical	—	primeFactorsList minFac	—	primeFactorsList.eq_3
primeFactorsList_chain 📖	mathematical	—	primeFactorsList	—	isChain_cons_primeFactorsList
primeFactorsList_chain' 📖	mathematical	—	primeFactorsList	—	isChain_primeFactorsList
primeFactorsList_chain_2 📖	mathematical	—	primeFactorsList	—	isChain_two_cons_primeFactorsList
primeFactorsList_eq_nil 📖	mathematical	—	primeFactorsList	—	primeFactorsList.eq_3 primeFactorsList_zero primeFactorsList_one
primeFactorsList_ne_nil 📖	—	—	—	—	primeFactorsList_eq_nil
primeFactorsList_one 📖	mathematical	—	primeFactorsList	—	primeFactorsList.eq_2
primeFactorsList_prime 📖	mathematical	Prime	primeFactorsList	—	Prime.two_le primeFactorsList.eq_3 prime_def_minFac Prime.pos
primeFactorsList_sorted 📖	mathematical	—	List.SortedLE instPreorder primeFactorsList	—	List.IsChain.sortedLE isChain_primeFactorsList
primeFactorsList_sublist_of_dvd 📖	mathematical	—	primeFactorsList	—	primeFactorsList_sublist_right right_ne_zero_of_mul
primeFactorsList_sublist_right 📖	mathematical	—	primeFactorsList	—	primeFactorsList_zero MulZeroClass.zero_mul List.sublist_of_subperm_of_pairwise perm_primeFactorsList_mul List.SortedLE.pairwise primeFactorsList_sorted
primeFactorsList_subset_of_dvd 📖	mathematical	—	primeFactorsList	—	primeFactorsList_sublist_of_dvd
primeFactorsList_subset_right 📖	mathematical	—	primeFactorsList	—	primeFactorsList_sublist_right
primeFactorsList_two 📖	mathematical	—	primeFactorsList	—	primeFactorsList.eq_3 zero_add minFac_two primeFactorsList_one
primeFactorsList_unique 📖	mathematical	instOne Prime	primeFactorsList	—	perm_of_prod_eq_prod instIsCancelMulZero Unique.instSubsingleton prod_primeFactorsList Prime.ne_zero List.prod_eq_zero_iff instNontrivial IsDomain.to_noZeroDivisors instIsDomain prime_of_mem_primeFactorsList
primeFactorsList_zero 📖	mathematical	—	primeFactorsList	—	primeFactorsList.eq_1
prime_of_mem_primeFactorsList 📖	mathematical	primeFactorsList	Prime	—	primeFactorsList_zero instIsEmptyFalse primeFactorsList_one factors_lemma primeFactorsList.eq_3 minFac_prime
prod_primeFactorsList 📖	mathematical	—	instOne primeFactorsList	—	primeFactorsList_zero primeFactorsList_one factors_lemma minFac_pos minFac_dvd instCharZero instAtLeastTwoHAddOfNat MulZeroClass.zero_mul primeFactorsList.eq_3
replicate_subperm_primeFactorsList_iff 📖	mathematical	Prime	primeFactorsList Monoid.toNatPow instMonoid	—	pow_zero Unique.instSubsingleton List.subperm_iff prod_primeFactorsList List.Perm.prod_eq List.prod_replicate List.Sublist.prod_dvd_prod mul_assoc perm_primeFactorsList_mul primeFactorsList_prime dvd_mul_right

Nat.Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
primeFactorsList_pow 📖	mathematical	Nat.Prime	Nat.primeFactorsList Monoid.toNatPow Nat.instMonoid	—	Nat.primeFactorsList_unique List.prod_replicate

---

← Back to Index