PrimeFin

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

Statistics

Metric	Count
Definitions `primeFactors`	1
Theorems `disjoint_primeFactors`, `primeFactors_mul`, `mem_primeFactors`, `mem_primeFactors'`, `mem_primeFactors_self`, `primeFactors`, `countable`, `infinite`, `disjoint_primeFactors`, `dvd_of_mem_primeFactors`, `infinite_setOf_prime`, `le_of_mem_primeFactors`, `mem_primeFactors`, `mem_primeFactors_iff_mem_primeFactorsList`, `mem_primeFactors_of_ne_zero`, `nonempty_primeFactors`, `pos_of_mem_primeFactors`, `primeFactors_eq_empty`, `primeFactors_gcd`, `primeFactors_mono`, `primeFactors_mul`, `primeFactors_one`, `primeFactors_pow`, `primeFactors_pow_succ`, `primeFactors_prime_pow`, `primeFactors_zero`, `prime_of_mem_primeFactors`, `toFinset_factors`	28
Total	29

Nat

Definitions

Name	Category	Theorems
`primeFactors` 📖	CompOp	62 math math: `prod_primeFactors_gcd_mul_prod_primeFactors_mul`, `isPrimePow_iff_card_primeFactors_eq_one`, `DirichletCharacter.LFunction_changeLevel`, `primeFactors_subset_of_mem_smoothNumbers`, `primeFactors_pow_succ`, `prod_primeFactors_of_squarefree`, `totient_eq_mul_prod_factors`, `prod_primeFactors_dvd`, `primeFactors_mono`, `DirichletCharacter.LSeries_changeLevel`, `primeFactors_eq_to_filter_divisors_prime`, `primeFactors_div_gcd`, `pairwise_coprime_pow_primeFactors_factorization`, `support_factorization`, `IsCyclotomicExtension.Rat.discr`, `primeFactors_gcd`, `DirichletCharacter.LFunctionTrivChar_eq_mul_riemannZeta`, `ArithmeticFunction.IsMultiplicative.prod_primeFactors`, `primeFactors_zero`, `mem_primeFactors_of_ne_zero`, `ArithmeticFunction.sigma_eq_prod_primeFactors_sum_range_factorization_pow_mul`, `toFinset_factors`, `isNilpotent_of_finite_tfae`, `ArithmeticFunction.prodPrimeFactors_apply`, `card_divisors`, `IsCyclotomicExtension.Rat.natAbs_discr`, `mem_factoredNumbers_iff_primeFactors_subset`, `Prime.mem_primeFactors_self`, `primeFactors_one`, `Prime.mem_primeFactors`, `prod_pow_primeFactors_factorization`, `primeFactors_subset_of_mem_factoredNumbers`, `prod_factorization_eq_prod_primeFactors`, `primeFactors_eq_empty`, `mem_primeFactors_iff_mem_primeFactorsList`, `sum_divisors`, `nonempty_primeFactors`, `prod_primeFactors_prod_factorization`, `disjoint_primeFactors`, `ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_add_of_squarefree`, `UniqueFactorizationMonoid.primeFactors_eq_natPrimeFactors`, `mem_smoothNumbers_iff_primeFactors_subset`, `primeFactors_pow`, `primeFactors_mul`, `DirichletCharacter.LFunctionTrivChar_residue_one`, `Coprime.disjoint_primeFactors`, `ArithmeticFunction.carmichael_factorization`, `primeFactors_filter_dvd_of_dvd`, `Prime.primeFactors`, `Prime.mem_primeFactors'`, `totient_eq_div_primeFactors_mul`, `primeFactors_prime_pow`, `not_isPrimePow_iff_nontrivial_of_two_le`, `primeFactors_prod`, `ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_sub_of_squarefree`, `mem_primeFactors`, `Coprime.primeFactors_mul`, `sum_primeFactors_gcd_add_sum_primeFactors_mul`, `prime_pow_pow_totient_ediv_prod`, `prod_primeFactors_pow_totient_ediv_dvd`, `totient_mul_prod_primeFactors`, `BoundingSieve.prod_primeFactors_nu`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_primeFactors` 📖	mathematical	—	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `primeFactors`	—	—
`dvd_of_mem_primeFactors` 📖	—	`Finset` `Finset.instMembership` `primeFactors`	—	—	`mem_primeFactors`
`infinite_setOf_prime` 📖	mathematical	—	`Set.Infinite` `setOf` `Prime`	—	`Set.infinite_of_not_bddAbove` `SemilatticeSup.instIsDirectedOrder` `not_bddAbove_setOf_prime`
`le_of_mem_primeFactors` 📖	—	`Finset` `Finset.instMembership` `primeFactors`	—	—	`Ne.bot_lt` `mem_primeFactors` `dvd_of_mem_primeFactors`
`mem_primeFactors` 📖	mathematical	—	`Finset` `Finset.instMembership` `primeFactors` `Prime`	—	—
`mem_primeFactors_iff_mem_primeFactorsList` 📖	mathematical	—	`Finset` `Finset.instMembership` `primeFactors` `primeFactorsList`	—	—
`mem_primeFactors_of_ne_zero` 📖	mathematical	—	`Finset` `Finset.instMembership` `primeFactors` `Prime`	—	—
`nonempty_primeFactors` 📖	mathematical	—	`Finset.Nonempty` `primeFactors`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₁` `primeFactors_eq_empty`
`pos_of_mem_primeFactors` 📖	—	`Finset` `Finset.instMembership` `primeFactors`	—	—	`Prime.pos` `prime_of_mem_primeFactors`
`primeFactors_eq_empty` 📖	mathematical	—	`primeFactors` `Finset` `Finset.instEmptyCollection`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `exists_prime_and_dvd` `mem_primeFactors` `primeFactors_zero` `primeFactors_one`
`primeFactors_gcd` 📖	mathematical	—	`primeFactors` `Finset` `Finset.instInter`	—	—
`primeFactors_mono` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `primeFactors`	—	`Dvd.dvd.trans`
`primeFactors_mul` 📖	mathematical	—	`primeFactors` `Finset` `Finset.instUnion`	—	`Finset.ext` `mem_primeFactorsList_mul`
`primeFactors_one` 📖	mathematical	—	`primeFactors` `Finset` `Finset.instEmptyCollection`	—	`Finset.ext` `Prime.ne_one`
`primeFactors_pow` 📖	mathematical	—	`primeFactors` `Monoid.toNatPow` `instMonoid`	—	`primeFactors_pow_succ`
`primeFactors_pow_succ` 📖	mathematical	—	`primeFactors` `Monoid.toNatPow` `instMonoid`	—	`eq_or_ne` `zero_pow` `primeFactors_zero` `zero_add` `pow_one` `primeFactors_mul` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsDomain` `Finset.union_idempotent`
`primeFactors_prime_pow` 📖	mathematical	`Prime`	`primeFactors` `Monoid.toNatPow` `instMonoid` `Finset` `Finset.instSingleton`	—	`primeFactors_pow` `Prime.primeFactors`
`primeFactors_zero` 📖	mathematical	—	`primeFactors` `Finset` `Finset.instEmptyCollection`	—	`Finset.ext`
`prime_of_mem_primeFactors` 📖	mathematical	`Finset` `Finset.instMembership` `primeFactors`	`Prime`	—	`mem_primeFactors`
`toFinset_factors` 📖	mathematical	—	`List.toFinset` `primeFactorsList` `primeFactors`	—	—

Nat.Coprime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_primeFactors` 📖	mathematical	—	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `Nat.primeFactors`	—	`List.disjoint_toFinset_iff_disjoint` `Nat.coprime_primeFactorsList_disjoint`
`primeFactors_mul` 📖	mathematical	—	`Nat.primeFactors` `Finset` `Finset.instUnion`	—	`List.toFinset.ext` `Nat.mem_primeFactorsList_mul_of_coprime` `List.toFinset_union`

Nat.Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_primeFactors` 📖	mathematical	`Nat.Prime`	`Finset` `Finset.instMembership` `Nat.primeFactors`	—	`Nat.mem_primeFactors`
`mem_primeFactors'` 📖	mathematical	`Nat.Prime`	`Finset` `Finset.instMembership` `Nat.primeFactors`	—	`mem_primeFactors`
`mem_primeFactors_self` 📖	mathematical	`Nat.Prime`	`Finset` `Finset.instMembership` `Nat.primeFactors`	—	`mem_primeFactors` `ne_zero`
`primeFactors` 📖	mathematical	`Nat.Prime`	`Nat.primeFactors` `Finset` `Finset.instSingleton`	—	`Nat.primeFactorsList_prime` `List.toFinset_cons` `Finset.instLawfulSingleton`

Nat.Primes

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`countable` 📖	mathematical	—	`Countable` `Nat.Primes`	—	`coe_nat_injective`
`infinite` 📖	mathematical	—	`Infinite` `Nat.Primes`	—	`Set.Infinite.to_subtype` `Nat.infinite_setOf_prime`

---

← Back to Index