Documentation Verification Report

PrimePow

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

Statistics

Metric	Count
Definitions `prodNatEquiv`	1
Theorems `exists_ordCompl_eq_one`, `minFac_pow_factorization_eq`, `isPrimePow_dvd_mul`, `coe_prodNatEquiv_apply`, `prodNatEquiv_apply`, `prodNatEquiv_symm_apply`, `exists_base_eq_prime_pow_of_prime_pow_eq_base_pow`, `exponent_dvd_of_prime_pow_eq_pow`, `exponent_eq_exponent_mul_factorization_of_prime_pow_eq_base_pow`, `mul_divisors_filter_prime_pow`, `not_isPrimePow_iff_nontrivial_of_two_le`, `exists_ordCompl_eq_one_iff_isPrimePow`, `isPrimePow_iff_card_primeFactors_eq_one`, `isPrimePow_iff_factorization_eq_single`, `isPrimePow_iff_minFac_pow_factorization_eq`, `isPrimePow_iff_unique_prime_dvd`, `isPrimePow_of_minFac_pow_factorization_eq`, `isPrimePow_pow_iff`	18
Total	19

IsPrimePow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_ordCompl_eq_one` 📖	mathematical	`IsPrimePow` `Nat.instCommMonoidWithZero`	`Nat.Prime` `Monoid.toNatPow` `Nat.instMonoid` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instFunLike` `Nat.factorization`	—	`eq_or_ne` `not_isPrimePow_zero` `IsDomain.to_noZeroDivisors` `Nat.instIsDomain` `isPrimePow_iff_factorization_eq_single` `em'` `Nat.factorization_eq_zero_of_not_prime` `Finsupp.single_eq_same` `LT.lt.ne'` `Nat.eq_of_factorization_eq` `Nat.ordCompl_pos` `Nat.factorization_ordCompl` `Finsupp.erase_single` `Nat.factorization_one`
`minFac_pow_factorization_eq` 📖	mathematical	`IsPrimePow` `Nat.instCommMonoidWithZero`	`Monoid.toNatPow` `Nat.instMonoid` `Nat.minFac` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instFunLike` `Nat.factorization`	—	`Nat.Prime.pow_minFac` `Nat.prime_iff` `LT.lt.ne'` `Nat.Prime.factorization_pow` `Finsupp.single_eq_same`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_base_eq_prime_pow_of_prime_pow_eq_base_pow` 📖	—	`Prime` `Monoid.toNatPow` `instMonoid`	—	—	`exponent_dvd_of_prime_pow_eq_pow` `pow_left_injective` `pow_mul'`
`exponent_dvd_of_prime_pow_eq_pow` 📖	—	`Prime` `Monoid.toNatPow` `instMonoid`	—	—	`Dvd.intro` `exponent_eq_exponent_mul_factorization_of_prime_pow_eq_base_pow`
`exponent_eq_exponent_mul_factorization_of_prime_pow_eq_base_pow` 📖	mathematical	`Prime` `Monoid.toNatPow` `instMonoid`	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `instMulZeroClass` `Finsupp.instFunLike` `factorization`	—	`Finsupp.single_eq_same` `factorization_pow` `Prime.factorization_pow`
`mul_divisors_filter_prime_pow` 📖	mathematical	—	`Finset.filter` `IsPrimePow` `instCommMonoidWithZero` `instDecidableIsPrimePowNat` `divisors` `Finset` `Finset.instUnion`	—	`eq_or_ne` `Finset.filter.congr_simp` `mul_one` `divisors_zero` `Finset.filter_empty` `divisors_one` `Finset.empty_union` `Finset.filter_singleton` `MulZeroClass.mul_zero` `Finset.union_empty` `Finset.ext` `Coprime.isPrimePow_dvd_mul`
`not_isPrimePow_iff_nontrivial_of_two_le` 📖	mathematical	—	`IsPrimePow` `instCommMonoidWithZero` `Finset.Nontrivial` `primeFactors`	—	`isPrimePow_iff_card_primeFactors_eq_one` `Finset.one_lt_card_iff_nontrivial`

Nat.Coprime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPrimePow_dvd_mul` 📖	—	`IsPrimePow` `Nat.instCommMonoidWithZero`	—	—	`eq_or_ne` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `isPrimePow_nat_iff` `Nat.Prime.pow_dvd_iff_le_factorization` `mul_ne_zero` `IsDomain.to_noZeroDivisors` `Nat.instIsDomain` `Nat.factorization_mul` `Finsupp.notMem_support_iff` `not_and_or` `Finset.mem_inter` `Disjoint.le_bot` `disjoint_primeFactors` `zero_add` `Nat.instCanonicallyOrderedAdd` `add_zero` `Dvd.dvd.trans` `dvd_mul_right` `dvd_refl` `dvd_mul_left`

Nat.Primes

Definitions

Name	Category	Theorems
`prodNatEquiv` 📖	CompOp	3 math math: `prodNatEquiv_symm_apply`, `prodNatEquiv_apply`, `coe_prodNatEquiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_prodNatEquiv_apply` 📖	mathematical	—	`IsPrimePow` `Nat.instCommMonoidWithZero` `DFunLike.coe` `Equiv` `Nat.Primes` `EquivLike.toFunLike` `Equiv.instEquivLike` `prodNatEquiv` `Monoid.toNatPow` `Nat.instMonoid` `Nat.Prime`	—	—
`prodNatEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Nat.Primes` `IsPrimePow` `Nat.instCommMonoidWithZero` `EquivLike.toFunLike` `Equiv.instEquivLike` `prodNatEquiv` `Monoid.toNatPow` `Nat.instMonoid` `Nat.Prime` `Prime` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero` `Nat.prime_iff` `Subtype.prop`	—	—
`prodNatEquiv_symm_apply` 📖	mathematical	`IsPrimePow` `Nat.instCommMonoidWithZero`	`DFunLike.coe` `Equiv` `Nat.Primes` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `prodNatEquiv` `Nat.Prime` `Nat.minFac` `Nat.minFac_prime` `IsPrimePow.ne_one` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instFunLike` `Nat.factorization`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_ordCompl_eq_one_iff_isPrimePow` 📖	mathematical	—	`IsPrimePow` `Nat.instCommMonoidWithZero` `Nat.Prime` `Monoid.toNatPow` `Nat.instMonoid` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instFunLike` `Nat.factorization`	—	`IsPrimePow.exists_ordCompl_eq_one` `isPrimePow_nat_iff` `Nat.ordProj_dvd` `Mathlib.Tactic.Contrapose.contrapose₂` `pow_zero`
`isPrimePow_iff_card_primeFactors_eq_one` 📖	mathematical	—	`IsPrimePow` `Nat.instCommMonoidWithZero` `Finset.card` `Nat.primeFactors`	—	`Nat.instCanonicallyOrderedAdd`
`isPrimePow_iff_factorization_eq_single` 📖	mathematical	—	`IsPrimePow` `Nat.instCommMonoidWithZero` `Nat.factorization` `Finsupp.single` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	`isPrimePow_nat_iff` `Nat.Prime.factorization_pow` `Nat.factorization_zero` `LT.lt.ne'` `Nat.eq_pow_of_factorization_eq_single` `Nat.prime_of_mem_primeFactors` `Finsupp.mem_support_iff` `Finsupp.single_eq_same`
`isPrimePow_iff_minFac_pow_factorization_eq` 📖	mathematical	—	`IsPrimePow` `Nat.instCommMonoidWithZero` `Monoid.toNatPow` `Nat.instMonoid` `Nat.minFac` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instFunLike` `Nat.factorization`	—	`IsPrimePow.minFac_pow_factorization_eq` `isPrimePow_of_minFac_pow_factorization_eq`
`isPrimePow_iff_unique_prime_dvd` 📖	mathematical	—	`IsPrimePow` `Nat.instCommMonoidWithZero` `ExistsUnique` `Nat.Prime`	—	`isPrimePow_nat_iff` `dvd_pow_self` `LT.lt.ne'` `Nat.prime_dvd_prime_iff_eq` `Nat.Prime.dvd_of_dvd_pow` `eq_or_ne` `Nat.prime_two` `dvd_zero` `Nat.prime_three` `Nat.Prime.factorization_pos_of_dvd` `Nat.ordProj_dvd` `Nat.dvd_of_primeFactorsList_subperm` `Nat.Prime.primeFactorsList_pow` `Nat.mem_primeFactorsList` `Nat.primeFactorsList_count_eq`
`isPrimePow_of_minFac_pow_factorization_eq` 📖	mathematical	`Monoid.toNatPow` `Nat.instMonoid` `Nat.minFac` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instFunLike` `Nat.factorization`	`IsPrimePow` `Nat.instCommMonoidWithZero`	—	`eq_or_ne` `Nat.factorization_zero` `pow_zero` `Nat.Prime.prime` `Nat.minFac_prime` `Nat.instCanonicallyOrderedAdd`
`isPrimePow_pow_iff` 📖	mathematical	—	`IsPrimePow` `Nat.instCommMonoidWithZero` `Monoid.toNatPow` `Nat.instMonoid`	—	`existsUnique_congr`

---

← Back to Index