Divisors

📁 Source: Mathlib/NumberTheory/Divisors.lean

Statistics

Metric	Count
Definitions divisorsAntidiag, divisors, divisorsAntidiagonal, divisorsAntidiagonalList, properDivisors	5
Theorems divisorsAntidiag_natCast, divisorsAntidiag_neg, divisorsAntidiag_neg_natCast, divisorsAntidiag_ofNat, divisorsAntidiag_zero, divisorsAntidiagonal_four, divisorsAntidiagonal_one, divisorsAntidiagonal_three, divisorsAntidiagonal_two, map_neg_divisorsAntidiag, map_prodComm_divisorsAntidiag, mem_divisorsAntidiag, mul_mem_one_two_three_iff, mul_mem_zero_one_two_three_four_iff, neg_mem_divisorsAntidiag, prodMk_mem_divisorsAntidiag, swap_mem_divisorsAntidiag, divisors, prod_divisors, prod_properDivisors, properDivisors, sum_divisors, sum_properDivisors, card_divisors_le_self, cons_self_properDivisors, disjoint_divisors_filter_isPrimePow, divisor_le, divisorsAntidiagonalList_one, divisorsAntidiagonalList_zero, divisorsAntidiagonal_eq_prod_filter_of_le, divisorsAntidiagonal_one, divisorsAntidiagonal_zero, divisors_eq_empty, divisors_filter_dvd_of_dvd, divisors_inj, divisors_injective, divisors_one, divisors_prime_pow, divisors_subset_of_dvd, divisors_subset_properDivisors, divisors_zero, dvd_of_mem_divisors, eq_properDivisors_of_subset_of_sum_eq_sum, filter_dvd_eq_divisors, filter_dvd_eq_properDivisors, fst_mem_divisors_of_mem_antidiagonal, image_div_divisors_eq_divisors, image_fst_divisorsAntidiagonal, image_snd_divisorsAntidiagonal, insert_self_properDivisors, left_ne_zero_of_mem_divisorsAntidiagonal, map_div_left_divisors, map_div_right_divisors, map_swap_divisorsAntidiagonal, mem_divisors, mem_divisorsAntidiagonal, mem_divisorsAntidiagonalList, mem_divisors_prime_pow, mem_divisors_self, mem_properDivisors, mem_properDivisors_iff_exists, mem_properDivisors_prime_pow, ne_zero_of_mem_divisors, ne_zero_of_mem_divisorsAntidiagonal, nodup_divisorsAntidiagonalList, nonempty_divisors, nonempty_properDivisors, one_lt_div_of_mem_properDivisors, one_lt_of_mem_properDivisors, one_mem_divisors, one_mem_properDivisors_iff_one_lt, pairwise_divisorsAntidiagonalList_fst, pairwise_divisorsAntidiagonalList_snd, perfect_iff_sum_divisors_eq_two_mul, perfect_iff_sum_properDivisors, pos_of_mem_divisors, pos_of_mem_properDivisors, primeFactors_eq_to_filter_divisors_prime, primeFactors_filter_dvd_of_dvd, prodMk_mem_divisorsAntidiag, prod_div_divisors, prod_divisorsAntidiagonal, prod_divisorsAntidiagonal', prod_divisors_prime_pow, prod_properDivisors_prime_pow, properDivisors_eq_empty, properDivisors_eq_singleton_one_iff_prime, properDivisors_one, properDivisors_prime_pow, properDivisors_subset_divisors, properDivisors_zero, reverse_divisorsAntidiagonalList, right_ne_zero_of_mem_divisorsAntidiagonal, self_notMem_properDivisors, snd_mem_divisors_of_mem_antidiagonal, sortedGT_map_snd_divisorsAntidiagonalList, sortedLT_map_fst_divisorsAntidiagonalList, sorted_divisorsAntidiagonalList_fst, sorted_divisorsAntidiagonalList_snd, sum_div_divisors, sum_divisorsAntidiagonal, sum_divisorsAntidiagonal', sum_divisors_eq_sum_properDivisors_add_self, sum_divisors_prime_pow, sum_properDivisors_dvd, sum_properDivisors_eq_one_iff_prime, sum_properDivisors_prime_nsmul, sup_divisors_id, swap_mem_divisorsAntidiagonal, swap_mem_divisorsAntidiagonalList, toFinset_divisorsAntidiagonalList, val_divisorsAntidiagonal	112
Total	117

Int

Definitions

Name	Category	Theorems
divisorsAntidiag 📖	CompOp	15 math math: mem_divisorsAntidiag, prodMk_mem_divisorsAntidiag, map_prodComm_divisorsAntidiag, divisorsAntidiagonal_three, divisorsAntidiag_natCast, divisorsAntidiagonal_four, divisorsAntidiagonal_two, divisorsAntidiagonal_one, neg_mem_divisorsAntidiag, divisorsAntidiag_neg, divisorsAntidiag_ofNat, swap_mem_divisorsAntidiag, divisorsAntidiag_zero, divisorsAntidiag_neg_natCast, map_neg_divisorsAntidiag

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
divisorsAntidiag_natCast 📖	mathematical	—	divisorsAntidiag Finset.disjUnion Finset.map Function.Embedding.prodMap Nat.castEmbedding AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instRing instCharZero Nat.divisorsAntidiagonal Function.Embedding.trans Equiv.toEmbedding Equiv.neg HasDistribNeg.toInvolutiveNeg Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing NonUnitalNonAssocRing.toHasDistribNeg	—	—
divisorsAntidiag_neg 📖	mathematical	—	divisorsAntidiag Finset.map Function.Embedding.prodMap Function.Embedding.refl Equiv.toEmbedding Equiv.neg HasDistribNeg.toInvolutiveNeg Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing NonUnitalNonAssocRing.toHasDistribNeg	—	Finset.ext neg_zero mul_neg
divisorsAntidiag_neg_natCast 📖	mathematical	—	divisorsAntidiag Finset.disjUnion Finset.map Function.Embedding.prodMap Nat.castEmbedding AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instRing instCharZero Function.Embedding.trans Equiv.toEmbedding Equiv.neg HasDistribNeg.toInvolutiveNeg Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing NonUnitalNonAssocRing.toHasDistribNeg Nat.divisorsAntidiagonal	—	instCharZero
divisorsAntidiag_ofNat 📖	mathematical	—	divisorsAntidiag Finset.disjUnion Finset.map Function.Embedding.prodMap Nat.castEmbedding AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instRing instCharZero Nat.divisorsAntidiagonal Function.Embedding.trans Equiv.toEmbedding Equiv.neg HasDistribNeg.toInvolutiveNeg Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing NonUnitalNonAssocRing.toHasDistribNeg	—	—
divisorsAntidiag_zero 📖	mathematical	—	divisorsAntidiag Finset Finset.instEmptyCollection	—	—
divisorsAntidiagonal_four 📖	mathematical	—	divisorsAntidiag Finset Finset.instInsert Finset.instSingleton	—	—
divisorsAntidiagonal_one 📖	mathematical	—	divisorsAntidiag Finset Finset.instInsert Finset.instSingleton	—	—
divisorsAntidiagonal_three 📖	mathematical	—	divisorsAntidiag Finset Finset.instInsert Finset.instSingleton	—	—
divisorsAntidiagonal_two 📖	mathematical	—	divisorsAntidiag Finset Finset.instInsert Finset.instSingleton	—	—
map_neg_divisorsAntidiag 📖	mathematical	—	Finset.map Equiv.toEmbedding Equiv.neg Prod.instInvolutiveNeg HasDistribNeg.toInvolutiveNeg Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing NonUnitalNonAssocRing.toHasDistribNeg divisorsAntidiag	—	Finset.ext mul_neg mul_comm neg_neg
map_prodComm_divisorsAntidiag 📖	mathematical	—	Finset.map Equiv.toEmbedding Equiv.prodComm divisorsAntidiag	—	Finset.ext
mem_divisorsAntidiag 📖	mathematical	—	Finset Finset.instMembership divisorsAntidiag	—	instCharZero Finset.disjUnion_eq_union instIsStrictOrderedRing MulZeroClass.mul_zero mul_neg neg_mul neg_neg Nat.cast_one MulZeroClass.zero_mul IsDomain.to_noZeroDivisors Nat.instIsDomain one_mul neg_add_rev Nat.cast_zero Nat.cast_mul Nat.cast_add
mul_mem_one_two_three_iff 📖	mathematical	—	Set Set.instMembership Set.instInsert Set.instSingletonSet	—	instCharZero Nat.instAtLeastTwoHAddOfNat
mul_mem_zero_one_two_three_four_iff 📖	mathematical	—	Set Set.instMembership Set.instInsert Set.instSingletonSet	—	instCharZero Nat.instAtLeastTwoHAddOfNat IsDomain.to_noZeroDivisors instIsDomain
neg_mem_divisorsAntidiag 📖	mathematical	—	Finset Finset.instMembership divisorsAntidiag Prod.instNeg	—	mul_neg neg_mul neg_neg
prodMk_mem_divisorsAntidiag 📖	mathematical	—	Finset Finset.instMembership divisorsAntidiag	—	—
swap_mem_divisorsAntidiag 📖	mathematical	—	Finset Finset.instMembership divisorsAntidiag	—	mul_comm

Nat

Definitions

Name	Category	Theorems
divisors 📖	CompOp	96 math math: divisorsHom_apply, divisors_filter_squarefree_of_squarefree, IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots, divisors_prime_pow, prod_divisorsAntidiagonal', ArithmeticFunction.sigma_apply, map_div_left_divisors, ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq, divisors_subset_of_dvd, Polynomial.prod_cyclotomic_eq_X_pow_sub_one, mem_divisors, ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on_of_nonzero, ArithmeticFunction.sigma_zero_apply, sum_totient, divisors_card_eq_one_iff, divisors_mul, primeFactors_eq_to_filter_divisors_prime, Prime.sum_divisors, List.nat_divisors_prod, snd_mem_divisors_of_mem_antidiagonal, one_mem_divisors, disjoint_divisors_filter_isPrimePow, Polynomial.prod_cyclotomic'_eq_X_pow_sub_one, ArithmeticFunction.sigma_one_apply, perfect_iff_sum_divisors_eq_two_mul, image_div_divisors_eq_divisors, properDivisors_subset_divisors, ArithmeticFunction.vonMangoldt_sum, ArithmeticFunction.sum_divisorsAntidiagonal_eq_sum_divisors, divisors_filter_dvd_of_dvd, image_snd_divisorsAntidiagonal, divisors_eq_empty, map_div_right_divisors, Finset.nat_divisors_prod, BoundingSieve.siftedSum_le_sum_of_upperMoebius, divisors_injective, ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq, ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq_on, sum_divisors_filter_squarefree, ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq, prod_divisors_prime_pow, cons_self_properDivisors, sum_divisors_eq_sum_properDivisors_add_self, sum_divisorsAntidiagonal', card_divisors, sum_div_divisors, Coprime.card_divisors_mul, Polynomial.X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd, image_fst_divisorsAntidiagonal, ArithmeticFunction.coe_zeta_smul_apply, prod_divisorsAntidiagonal, filter_dvd_eq_divisors, Polynomial.prod_cyclotomic_eq_geom_sum, divisors_subset_properDivisors, Prime.prod_divisors, Prime.divisors, Multiset.nat_divisors_prod, ArithmeticFunction.sum_moebius_mul_log_eq, sum_divisors_prime_pow, ArithmeticFunction.coe_mul_zeta_apply, sup_divisors_id, card_divisors_le_self, divisors_inj, ArithmeticFunction.mul_zeta_apply, sum_divisors, nonempty_divisors, ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_add_of_squarefree, fst_mem_divisors_of_mem_antidiagonal, abundant_iff_sum_divisors, ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on, Prime.divisors_sq, mem_divisors_prime_pow, prod_div_divisors, insert_self_properDivisors, image_apply_finMulAntidiag, divisors_one, divisors_filter_squarefree, ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on', range_pow_padicValNat_subset_divisors', card_pair_lcm_eq, sum_card_addOrderOf_eq_card_nsmul_eq_zero, ArithmeticFunction.zeta_mul_apply, mem_divisors_self, Coprime.sum_divisors_mul, isRoot_of_unity_iff, ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_of_nonzero, mul_divisors_filter_prime_pow, sum_card_orderOf_eq_card_pow_eq_one, ArithmeticFunction.sigma_eq_sum_div, ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_sub_of_squarefree, finMulAntidiag_eq_piFinset_divisors_filter, range_pow_padicValNat_subset_divisors, ArithmeticFunction.coe_zeta_mul_apply, ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on, divisors_zero, sum_divisorsAntidiagonal
divisorsAntidiagonal 📖	CompOp	38 math math: swap_mem_divisorsAntidiagonal, prod_divisorsAntidiagonal', map_swap_divisorsAntidiagonal, map_div_left_divisors, ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq, sigmaAntidiagonalEquivProd_symm_apply_snd, LSeries.convolution_def, ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on_of_nonzero, ArithmeticFunction.smul_apply, mem_divisorsAntidiagonal, Int.divisorsAntidiag_natCast, toFinset_divisorsAntidiagonalList, LSeries.term_convolution, ArithmeticFunction.sum_divisorsAntidiagonal_eq_sum_divisors, image_snd_divisorsAntidiagonal, map_div_right_divisors, image_piFinTwoEquiv_finMulAntidiag, ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq, ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq_on, ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq, sum_divisorsAntidiagonal', image_fst_divisorsAntidiagonal, prod_divisorsAntidiagonal, sigmaAntidiagonalEquivProd_symm_apply_fst, Polynomial.cyclotomic_eq_prod_X_pow_sub_one_pow_moebius, divisorsAntidiagonal_eq_prod_filter_of_le, Int.divisorsAntidiag_ofNat, ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on, ArithmeticFunction.mul_apply, val_divisorsAntidiagonal, divisorsAntidiagonal_zero, divisorsAntidiagonal_one, ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on', ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_of_nonzero, prodMk_mem_divisorsAntidiag, ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on, Int.divisorsAntidiag_neg_natCast, sum_divisorsAntidiagonal
divisorsAntidiagonalList 📖	CompOp	14 math math: sortedLT_map_fst_divisorsAntidiagonalList, pairwise_divisorsAntidiagonalList_fst, reverse_divisorsAntidiagonalList, toFinset_divisorsAntidiagonalList, mem_divisorsAntidiagonalList, divisorsAntidiagonalList_one, swap_mem_divisorsAntidiagonalList, sorted_divisorsAntidiagonalList_snd, sortedGT_map_snd_divisorsAntidiagonalList, sorted_divisorsAntidiagonalList_fst, divisorsAntidiagonalList_zero, val_divisorsAntidiagonal, pairwise_divisorsAntidiagonalList_snd, nodup_divisorsAntidiagonalList
properDivisors 📖	CompOp	28 math math: mem_properDivisors_prime_pow, Polynomial.eq_cyclotomic_iff, properDivisors_zero, perfect_iff_sum_properDivisors, one_mem_properDivisors_iff_one_lt, properDivisors_one, properDivisors_eq_empty, mem_properDivisors_iff_exists, Prime.properDivisors, Polynomial.X_pow_sub_one_dvd_prod_cyclotomic, sum_properDivisors_eq_one_iff_prime, properDivisors_prime_pow, properDivisors_subset_divisors, properDivisors_eq_singleton_one_iff_prime, cons_self_properDivisors, Prime.sum_properDivisors, sum_divisors_eq_sum_properDivisors_add_self, Prime.prod_properDivisors, filter_dvd_eq_properDivisors, nonempty_properDivisors, prod_properDivisors_prime_pow, divisors_subset_properDivisors, self_notMem_properDivisors, mem_properDivisors, insert_self_properDivisors, sum_properDivisors_prime_nsmul, Polynomial.cyclotomic_eq_X_pow_sub_one_div, Polynomial.cyclotomic'_eq_X_pow_sub_one_div

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_divisors_le_self 📖	mathematical	—	Finset.card divisors	—	Finset.card_le_card card_Ico add_tsub_cancel_right instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
cons_self_properDivisors 📖	mathematical	—	Finset.cons properDivisors self_notMem_properDivisors divisors	—	self_notMem_properDivisors Finset.cons_eq_insert insert_self_properDivisors
disjoint_divisors_filter_isPrimePow 📖	mathematical	—	Disjoint Finset Finset.partialOrder Finset.instOrderBot Finset.filter IsPrimePow instCommMonoidWithZero instDecidableIsPrimePowNat divisors	—	IsPrimePow.ne_one eq_one_of_dvd_coprimes
divisor_le 📖	—	Finset Finset.instMembership divisors	—	—	instCanonicallyOrderedAdd instIsEmptyFalse
divisorsAntidiagonalList_one 📖	mathematical	—	divisorsAntidiagonalList	—	—
divisorsAntidiagonalList_zero 📖	mathematical	—	divisorsAntidiagonalList	—	—
divisorsAntidiagonal_eq_prod_filter_of_le 📖	mathematical	—	divisorsAntidiagonal Finset.filter SProd.sprod Finset Finset.instSProd Finset.Ioc instPreorder instLocallyFiniteOrder	—	Finset.ext mem_divisorsAntidiagonal Mathlib.Tactic.GCongr.and_right_mono le_imp_le_of_le_of_le le_refl IsOrderedRing.toPosMulMono IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRing PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono IsOrderedRing.toMulPosMono MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono
divisorsAntidiagonal_one 📖	mathematical	—	divisorsAntidiagonal Finset Finset.instSingleton	—	Finset.ext Unique.instSubsingleton
divisorsAntidiagonal_zero 📖	mathematical	—	divisorsAntidiagonal Finset Finset.instEmptyCollection	—	Finset.ext IsDomain.to_noZeroDivisors instIsDomain
divisors_eq_empty 📖	mathematical	—	divisors Finset Finset.instEmptyCollection	—	Mathlib.Tactic.Contrapose.contrapose_iff₁ nonempty_divisors
divisors_filter_dvd_of_dvd 📖	mathematical	—	Finset.filter divisors	—	Finset.ext ne_zero_of_dvd_ne_zero Dvd.dvd.trans
divisors_inj 📖	mathematical	—	divisors	—	divisors_injective
divisors_injective 📖	mathematical	—	Finset divisors	—	instCommutativeMax_mathlib instAssociativeMax_mathlib sup_divisors_id
divisors_one 📖	mathematical	—	divisors Finset Finset.instSingleton	—	Finset.ext
divisors_prime_pow 📖	mathematical	Prime	divisors Monoid.toNatPow instMonoid Finset.map pow_right_injective Prime.two_le Finset.range	—	Finset.ext pow_right_injective Prime.two_le mem_divisors_prime_pow instNoMaxOrder
divisors_subset_of_dvd 📖	mathematical	—	Finset Finset.instHasSubset divisors	—	Finset.subset_iff mem_divisors Dvd.dvd.trans
divisors_subset_properDivisors 📖	mathematical	—	Finset Finset.instHasSubset divisors properDivisors	—	Finset.subset_iff mem_properDivisors Dvd.dvd.trans mem_divisors lt_of_le_of_lt divisor_le lt_of_le_of_ne
divisors_zero 📖	mathematical	—	divisors Finset Finset.instEmptyCollection	—	Finset.ext
dvd_of_mem_divisors 📖	—	Finset Finset.instMembership divisors	—	—	mem_divisors
eq_properDivisors_of_subset_of_sum_eq_sum 📖	—	Finset Finset.instHasSubset properDivisors Finset.sum instAddCommMonoid	—	—	Finset.sum_congr Finset.subset_empty properDivisors_zero Finset.sum_sdiff Finset.Subset.antisymm Finset.sdiff_eq_empty_iff_subset Mathlib.Tactic.Contrapose.contrapose₁ zero_add add_assoc add_zero add_lt_add_left IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Finset.sum_lt_sum_of_nonempty instIsOrderedCancelAddMonoid pos_of_mem_properDivisors Finset.sdiff_subset Finset.sum_const_zero
filter_dvd_eq_divisors 📖	mathematical	—	Finset.filter Finset.range divisors	—	Finset.ext Ne.bot_lt
filter_dvd_eq_properDivisors 📖	mathematical	—	Finset.filter Finset.range properDivisors	—	Finset.ext Ne.bot_lt
fst_mem_divisors_of_mem_antidiagonal 📖	mathematical	Finset Finset.instMembership divisorsAntidiagonal	divisors	—	Dvd.intro mem_divisorsAntidiagonal
image_div_divisors_eq_divisors 📖	mathematical	—	Finset.image divisors	—	divisors_zero Finset.ext Finset.mem_image mem_divisors
image_fst_divisorsAntidiagonal 📖	mathematical	—	Finset.image divisorsAntidiagonal divisors	—	Finset.ext
image_snd_divisorsAntidiagonal 📖	mathematical	—	Finset.image divisorsAntidiagonal divisors	—	map_swap_divisorsAntidiagonal Finset.map_eq_image Finset.image_image image_fst_divisorsAntidiagonal
insert_self_properDivisors 📖	mathematical	—	Finset Finset.instInsert properDivisors divisors	—	divisors.eq_1 properDivisors.eq_1 Finset.insert_Ico_right_eq_Ico_add_one instNoMaxOrder Finset.filter_insert dvd_refl
left_ne_zero_of_mem_divisorsAntidiagonal 📖	—	Finset Finset.instMembership divisorsAntidiagonal	—	—	ne_zero_of_mem_divisorsAntidiagonal
map_div_left_divisors 📖	mathematical	—	Finset.map divisors divisorsAntidiagonal	—	Finset.map_injective Finset.ext map_swap_divisorsAntidiagonal map_div_right_divisors Finset.map_map
map_div_right_divisors 📖	mathematical	—	Finset.map divisors divisorsAntidiagonal	—	Finset.ext Ne.bot_lt left_ne_zero_of_mul dvd_mul_right
map_swap_divisorsAntidiagonal 📖	mathematical	—	Finset.map Equiv.toEmbedding Equiv.prodComm divisorsAntidiagonal	—	Finset.coe_map Equiv.coe_toEmbedding Equiv.coe_prodComm Set.image_swap_eq_preimage_swap Set.ext swap_mem_divisorsAntidiagonal
mem_divisors 📖	mathematical	—	Finset Finset.instMembership divisors	—	eq_or_ne Finset.filter.congr_simp zero_add Finset.Ico_eq_empty_of_le Finset.filter_empty filter_dvd_eq_divisors Ne.bot_lt
mem_divisorsAntidiagonal 📖	mathematical	—	Finset Finset.instMembership divisorsAntidiagonal	—	Finset.filterMap.congr_simp mul_ne_zero_iff IsDomain.to_noZeroDivisors instIsDomain mul_div_cancel_left₀ instMulDivCancelClass Ne.bot_lt
mem_divisorsAntidiagonalList 📖	mathematical	—	divisorsAntidiagonalList	—	List.mem_toFinset toFinset_divisorsAntidiagonalList mem_divisorsAntidiagonal
mem_divisors_prime_pow 📖	mathematical	Prime	Finset Finset.instMembership divisors Monoid.toNatPow instMonoid	—	mem_divisors dvd_prime_pow pow_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono instZeroLEOneClass Prime.pos
mem_divisors_self 📖	mathematical	—	Finset Finset.instMembership divisors	—	mem_divisors dvd_rfl
mem_properDivisors 📖	mathematical	—	Finset Finset.instMembership properDivisors	—	eq_or_ne Finset.filter.congr_simp Finset.Ico_eq_empty_of_le instCanonicallyOrderedAdd Finset.filter_empty filter_dvd_eq_properDivisors
mem_properDivisors_iff_exists 📖	mathematical	—	Finset Finset.instMembership properDivisors	—	one_lt_div_of_mem_properDivisors mem_properDivisors lt_mul_of_one_lt_right LinearOrderedCommMonoidWithZero.toPosMulStrictMono mul_ne_zero_iff IsDomain.to_noZeroDivisors instIsDomain
mem_properDivisors_prime_pow 📖	mathematical	Prime	Finset Finset.instMembership properDivisors Monoid.toNatPow instMonoid	—	mem_properDivisors dvd_prime_pow Prime.one_lt
ne_zero_of_mem_divisors 📖	—	Finset Finset.instMembership divisors	—	—	mem_divisors
ne_zero_of_mem_divisorsAntidiagonal 📖	—	Finset Finset.instMembership divisorsAntidiagonal	—	—	mem_divisorsAntidiagonal mul_ne_zero_iff IsDomain.to_noZeroDivisors instIsDomain
nodup_divisorsAntidiagonalList 📖	mathematical	—	divisorsAntidiagonalList	—	List.Pairwise.nodup pairwise_divisorsAntidiagonalList_fst
nonempty_divisors 📖	mathematical	—	Finset.Nonempty divisors	—	divisors_zero one_mem_divisors
nonempty_properDivisors 📖	mathematical	—	Finset.Nonempty properDivisors	—	one_lt_of_mem_properDivisors one_mem_properDivisors_iff_one_lt
one_lt_div_of_mem_properDivisors 📖	—	Finset Finset.instMembership properDivisors	—	—	mem_properDivisors mul_one
one_lt_of_mem_properDivisors 📖	—	Finset Finset.instMembership properDivisors	—	—	lt_of_le_of_lt pos_of_mem_properDivisors mem_properDivisors
one_mem_divisors 📖	mathematical	—	Finset Finset.instMembership divisors	—	Unique.instSubsingleton
one_mem_properDivisors_iff_one_lt 📖	mathematical	—	Finset Finset.instMembership properDivisors	—	mem_properDivisors one_dvd
pairwise_divisorsAntidiagonalList_fst 📖	mathematical	—	divisorsAntidiagonalList	—	List.SortedLT.pairwise List.sortedLT_range'
pairwise_divisorsAntidiagonalList_snd 📖	mathematical	—	divisorsAntidiagonalList	—	eq_or_ne List.SortedLT.pairwise List.sortedLT_range'
perfect_iff_sum_divisors_eq_two_mul 📖	mathematical	—	Perfect Finset.sum instAddCommMonoid divisors	—	perfect_iff_sum_properDivisors sum_divisors_eq_sum_properDivisors_add_self instAtLeastTwoHAddOfNat two_mul add_right_cancel AddRightCancelSemigroup.toIsRightCancelAdd
perfect_iff_sum_properDivisors 📖	mathematical	—	Perfect Finset.sum instAddCommMonoid properDivisors	—	—
pos_of_mem_divisors 📖	—	Finset Finset.instMembership divisors	—	—	zero_dvd_iff mem_divisors
pos_of_mem_properDivisors 📖	—	Finset Finset.instMembership properDivisors	—	—	pos_of_mem_divisors properDivisors_subset_divisors
primeFactors_eq_to_filter_divisors_prime 📖	mathematical	—	primeFactors Finset.filter Prime decidablePrime divisors	—	—
primeFactors_filter_dvd_of_dvd 📖	mathematical	—	Finset.filter primeFactors	—	Finset.filter.congr_simp primeFactors_eq_to_filter_divisors_prime Finset.filter_comm divisors_filter_dvd_of_dvd
prodMk_mem_divisorsAntidiag 📖	mathematical	—	Finset Finset.instMembership divisorsAntidiagonal	—	—
prod_div_divisors 📖	mathematical	—	Finset.prod divisors	—	Finset.prod_congr divisors_zero Finset.prod_const pow_zero Finset.prod_image mem_divisors Finset.mem_coe image_div_divisors_eq_divisors
prod_divisorsAntidiagonal 📖	mathematical	—	Finset.prod divisorsAntidiagonal divisors	—	map_div_right_divisors Finset.prod_map
prod_divisorsAntidiagonal' 📖	mathematical	—	Finset.prod divisorsAntidiagonal divisors	—	map_swap_divisorsAntidiagonal Finset.prod_map prod_divisorsAntidiagonal
prod_divisors_prime_pow 📖	mathematical	Prime	Finset.prod divisors Monoid.toNatPow instMonoid Finset.range	—	pow_right_injective Prime.two_le Finset.prod_congr divisors_prime_pow Finset.prod_map
prod_properDivisors_prime_pow 📖	mathematical	Prime	Finset.prod properDivisors Monoid.toNatPow instMonoid Finset.range	—	pow_right_injective Prime.two_le Finset.prod_congr properDivisors_prime_pow Finset.prod_map
properDivisors_eq_empty 📖	mathematical	—	properDivisors Finset Finset.instEmptyCollection	—	Mathlib.Tactic.Contrapose.contrapose_iff₁ nonempty_properDivisors
properDivisors_eq_singleton_one_iff_prime 📖	mathematical	—	properDivisors Finset Finset.instSingleton Prime	—	prime_def covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le instCanonicallyOrderedAdd Finset.mem_singleton mem_properDivisors nonpos_iff_eq_zero le_iff_eq_or_lt Prime.properDivisors
properDivisors_one 📖	mathematical	—	properDivisors Finset Finset.instEmptyCollection	—	properDivisors.eq_1 Finset.Ico_self Finset.filter_empty
properDivisors_prime_pow 📖	mathematical	Prime	properDivisors Monoid.toNatPow instMonoid Finset.map pow_right_injective Prime.two_le Finset.range	—	Finset.ext pow_right_injective Prime.two_le mem_properDivisors_prime_pow mem_properDivisors
properDivisors_subset_divisors 📖	mathematical	—	Finset Finset.instHasSubset properDivisors divisors	—	Finset.filter_subset_filter Finset.Ico_subset_Ico_right
properDivisors_zero 📖	mathematical	—	properDivisors Finset Finset.instEmptyCollection	—	Finset.ext instCanonicallyOrderedAdd
reverse_divisorsAntidiagonalList 📖	mathematical	—	divisorsAntidiagonalList	—	lt_asymm List.Perm.eq_of_pairwise' List.Pairwise.reverse pairwise_divisorsAntidiagonalList_snd pairwise_divisorsAntidiagonalList_fst nodup_divisorsAntidiagonalList List.Nodup.map Prod.swap_injective mul_comm
right_ne_zero_of_mem_divisorsAntidiagonal 📖	—	Finset Finset.instMembership divisorsAntidiagonal	—	—	ne_zero_of_mem_divisorsAntidiagonal
self_notMem_properDivisors 📖	mathematical	—	Finset Finset.instMembership properDivisors	—	—
snd_mem_divisors_of_mem_antidiagonal 📖	mathematical	Finset Finset.instMembership divisorsAntidiagonal	divisors	—	Dvd.intro_left mem_divisorsAntidiagonal
sortedGT_map_snd_divisorsAntidiagonalList 📖	mathematical	—	List.SortedGT instPreorder divisorsAntidiagonalList	—	List.Pairwise.sortedGT pairwise_divisorsAntidiagonalList_snd
sortedLT_map_fst_divisorsAntidiagonalList 📖	mathematical	—	List.SortedLT instPreorder divisorsAntidiagonalList	—	List.Pairwise.sortedLT pairwise_divisorsAntidiagonalList_fst
sorted_divisorsAntidiagonalList_fst 📖	mathematical	—	divisorsAntidiagonalList	—	pairwise_divisorsAntidiagonalList_fst
sorted_divisorsAntidiagonalList_snd 📖	mathematical	—	divisorsAntidiagonalList	—	pairwise_divisorsAntidiagonalList_snd
sum_div_divisors 📖	mathematical	—	Finset.sum divisors	—	Finset.sum_congr divisors_zero Finset.sum_const zero_nsmul Finset.sum_image mem_divisors Finset.mem_coe image_div_divisors_eq_divisors
sum_divisorsAntidiagonal 📖	mathematical	—	Finset.sum divisorsAntidiagonal divisors	—	map_div_right_divisors Finset.sum_map
sum_divisorsAntidiagonal' 📖	mathematical	—	Finset.sum divisorsAntidiagonal divisors	—	map_swap_divisorsAntidiagonal Finset.sum_map sum_divisorsAntidiagonal
sum_divisors_eq_sum_properDivisors_add_self 📖	mathematical	—	Finset.sum instAddCommMonoid divisors properDivisors	—	Decidable.eq_or_ne Finset.sum_congr divisors_zero properDivisors_zero add_zero self_notMem_properDivisors cons_self_properDivisors Finset.sum_cons add_comm
sum_divisors_prime_pow 📖	mathematical	Prime	Finset.sum divisors Monoid.toNatPow instMonoid Finset.range	—	pow_right_injective Prime.two_le Finset.sum_congr divisors_prime_pow Finset.sum_map
sum_properDivisors_dvd 📖	—	Finset.sum instAddCommMonoid properDivisors	—	—	Finset.sum_congr properDivisors_zero zero_add properDivisors_one lt_of_le_of_ne Finset.mem_singleton eq_properDivisors_of_subset_of_sum_eq_sum Finset.singleton_subset_iff mem_properDivisors Finset.sum_singleton one_dvd
sum_properDivisors_eq_one_iff_prime 📖	mathematical	—	Finset.sum instAddCommMonoid properDivisors Prime	—	Finset.sum_congr properDivisors_zero zero_add properDivisors_one properDivisors_eq_singleton_one_iff_prime eq_properDivisors_of_subset_of_sum_eq_sum Finset.singleton_subset_iff one_mem_properDivisors_iff_one_lt Finset.sum_singleton
sum_properDivisors_prime_nsmul 📖	mathematical	Prime	Finset.sum properDivisors Monoid.toNatPow instMonoid Finset.range	—	pow_right_injective Prime.two_le Finset.sum_congr properDivisors_prime_pow Finset.sum_map
sup_divisors_id 📖	mathematical	—	Finset.sup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeNat instOrderBot divisors	—	le_antisymm Finset.sup_le divisor_le Decidable.eq_or_ne Finset.le_sup mem_divisors_self
swap_mem_divisorsAntidiagonal 📖	mathematical	—	Finset Finset.instMembership divisorsAntidiagonal	—	mem_divisorsAntidiagonal mul_comm Prod.swap.eq_1
swap_mem_divisorsAntidiagonalList 📖	mathematical	—	divisorsAntidiagonalList	—	mul_comm
toFinset_divisorsAntidiagonalList 📖	mathematical	—	List.toFinset divisorsAntidiagonalList divisorsAntidiagonal	—	divisorsAntidiagonalList.eq_1 divisorsAntidiagonal.eq_1 List.toFinset_filterMap List.toFinset_range'_1_1
val_divisorsAntidiagonal 📖	mathematical	—	Finset.val divisorsAntidiagonal Multiset.ofList divisorsAntidiagonalList	—	—

Nat.Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
divisors 📖	mathematical	Nat.Prime	Nat.divisors Finset Finset.instInsert Finset.instSingleton	—	Finset.ext Nat.mem_divisors Nat.dvd_prime ne_zero Finset.mem_insert Finset.mem_singleton
prod_divisors 📖	mathematical	Nat.Prime	Finset.prod Nat.divisors MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	Nat.self_notMem_properDivisors Nat.cons_self_properDivisors ne_zero Finset.prod_cons prod_properDivisors
prod_properDivisors 📖	mathematical	Nat.Prime	Finset.prod Nat.properDivisors	—	Finset.prod_congr properDivisors Finset.prod_singleton
properDivisors 📖	mathematical	Nat.Prime	Nat.properDivisors Finset Finset.instSingleton	—	Finset.erase_insert Nat.self_notMem_properDivisors Nat.insert_self_properDivisors ne_zero divisors Finset.pair_comm ne_one Finset.mem_singleton
sum_divisors 📖	mathematical	Nat.Prime	Finset.sum Nat.divisors AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Nat.self_notMem_properDivisors Nat.cons_self_properDivisors ne_zero Finset.sum_cons sum_properDivisors
sum_properDivisors 📖	mathematical	Nat.Prime	Finset.sum Nat.properDivisors	—	Finset.sum_congr properDivisors Finset.sum_singleton

---

← Back to Index