Documentation Verification Report

IsPrimePow

📁 Source: Mathlib/Algebra/IsPrimePow.lean

Statistics

Metric	Count
Definitions `IsPrimePow`, `instDecidableIsPrimePowNat`	2
Theorems `dvd`, `ne_one`, `ne_zero`, `not_unit`, `one_lt`, `pos`, `pow`, `two_le`, `not_isPrimePow`, `isPrimePow`, `isPrimePow`, `isPrimePow_def`, `isPrimePow_iff_pow_succ`, `isPrimePow_nat_iff`, `isPrimePow_nat_iff_bounded`, `isPrimePow_nat_iff_bounded_log`, `isPrimePow_nat_iff_bounded_log_minFac`, `not_isPrimePow_one`, `not_isPrimePow_zero`	19
Total	21

IsPrimePow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dvd` 📖	—	`IsPrimePow` `Nat.instCommMonoidWithZero`	—	—	—
`ne_one` 📖	—	`IsPrimePow`	—	—	`not_isPrimePow_one`
`ne_zero` 📖	—	`IsPrimePow`	—	—	`not_isPrimePow_zero`
`not_unit` 📖	mathematical	`IsPrimePow`	`IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	`Iff.not` `isUnit_pow_iff` `LT.lt.ne'` `Prime.not_unit`
`one_lt` 📖	—	`IsPrimePow` `Nat.instCommMonoidWithZero`	—	—	`two_le`
`pos` 📖	—	`IsPrimePow` `Nat.instCommMonoidWithZero`	—	—	`pos_of_gt` `Nat.instCanonicallyOrderedAdd` `two_le`
`pow` 📖	mathematical	`IsPrimePow`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	`mul_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Ne.bot_lt` `pow_mul'`
`two_le` 📖	—	`IsPrimePow` `Nat.instCommMonoidWithZero`	—	—	`not_isPrimePow_zero` `IsDomain.to_noZeroDivisors` `Nat.instIsDomain` `not_isPrimePow_one` `le_add_self` `Nat.instCanonicallyOrderedAdd`

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_isPrimePow` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	`IsPrimePow`	—	`IsPrimePow.not_unit`

Nat.Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPrimePow` 📖	mathematical	`Nat.Prime`	`IsPrimePow` `Nat.instCommMonoidWithZero`	—	`Prime.isPrimePow` `Nat.prime_iff`

Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPrimePow` 📖	mathematical	`Prime`	`IsPrimePow`	—	`zero_lt_one` `Nat.instZeroLEOneClass` `pow_one`

(root)

Definitions

Name	Category	Theorems
`IsPrimePow` 📖	MathDef	37 math math: `Nat.squarefree_and_prime_pow_iff_prime`, `Cardinal.isPrimePow_iff`, `FiniteField.isPrimePow_card`, `isPrimePow_iff_card_primeFactors_eq_one`, `IsUnit.not_isPrimePow`, `isPrimePow_iff_factorization_eq_single`, `Field.nonempty_iff`, `isPrimePow_iff_pow_succ`, `isPrimePow_nat_iff`, `Chebyshev.sum_PrimePow_eq_sum_sum`, `Nat.Primes.prodNatEquiv_apply`, `Nat.disjoint_divisors_filter_isPrimePow`, `isPrimePow_nat_iff_bounded`, `DivisorChain.isPrimePow_of_has_chain`, `ArithmeticFunction.vonMangoldt_pos_iff`, `Fintype.isPrimePow_card_of_field`, `isPrimePow_of_minFac_pow_factorization_eq`, `ArithmeticFunction.vonMangoldt_ne_zero_iff`, `not_isPrimePow_zero`, `isPrimePow_nat_iff_bounded_log`, `Fintype.nonempty_field_iff`, `Nat.Primes.coe_prodNatEquiv_apply`, `ArithmeticFunction.cardDistinctFactors_eq_one_iff`, `isPrimePow_iff_unique_prime_dvd`, `exists_ordCompl_eq_one_iff_isPrimePow`, `ArithmeticFunction.vonMangoldt_apply`, `not_isPrimePow_one`, `Prime.isPrimePow`, `Nat.Prime.isPrimePow`, `isPrimePow_def`, `ArithmeticFunction.vonMangoldt_eq_zero_iff`, `isPrimePow_nat_iff_bounded_log_minFac`, `isPrimePow_pow_iff`, `Nat.not_isPrimePow_iff_nontrivial_of_two_le`, `Nat.mul_divisors_filter_prime_pow`, `isPrimePow_iff_minFac_pow_factorization_eq`, `charP_zero_or_prime_power`
`instDecidableIsPrimePowNat` 📖	CompOp	4 math math: `Chebyshev.sum_PrimePow_eq_sum_sum`, `Nat.disjoint_divisors_filter_isPrimePow`, `ArithmeticFunction.vonMangoldt_apply`, `Nat.mul_divisors_filter_prime_pow`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPrimePow_def` 📖	mathematical	—	`IsPrimePow` `Prime` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	—
`isPrimePow_iff_pow_succ` 📖	mathematical	—	`IsPrimePow` `Prime` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `CommMonoidWithZero.toMonoidWithZero`	—	`isPrimePow_def` `Nat.succ_pos'`
`isPrimePow_nat_iff` 📖	mathematical	—	`IsPrimePow` `Nat.instCommMonoidWithZero` `Nat.Prime` `Monoid.toNatPow` `Nat.instMonoid`	—	—
`isPrimePow_nat_iff_bounded` 📖	mathematical	—	`IsPrimePow` `Nat.instCommMonoidWithZero` `Nat.Prime` `Monoid.toNatPow` `Nat.instMonoid`	—	`isPrimePow_nat_iff` `pow_one` `LT.lt.le` `Nat.Prime.one_lt`
`isPrimePow_nat_iff_bounded_log` 📖	mathematical	—	`IsPrimePow` `Nat.instCommMonoidWithZero` `Nat.log` `Monoid.toNatPow` `Nat.instMonoid` `Nat.Prime`	—	`isPrimePow_nat_iff` `Nat.log_pow` `Nat.log_mono` `Nat.AtLeastTwo.prop` `Nat.instAtLeastTwoHAddOfNat` `Nat.Prime.two_le`
`isPrimePow_nat_iff_bounded_log_minFac` 📖	mathematical	—	`IsPrimePow` `Nat.instCommMonoidWithZero` `Nat.log` `Monoid.toNatPow` `Nat.instMonoid` `Nat.minFac`	—	`isPrimePow_nat_iff_bounded_log` `eq_or_ne` `Nat.log_one_right` `Nat.instCanonicallyOrderedAdd` `pow_zero` `Nat.minFac_one` `one_pow` `Nat.Prime.pow_minFac` `LT.lt.ne'` `Nat.minFac_le`
`not_isPrimePow_one` 📖	mathematical	—	`IsPrimePow` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	—	`IsUnit.not_isPrimePow` `isUnit_one`
`not_isPrimePow_zero` 📖	mathematical	—	`IsPrimePow` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `CommMonoidWithZero.toMonoidWithZero`	—	`eq_zero_of_pow_eq_zero` `isReduced_of_noZeroDivisors`

---

← Back to Index