Theorems · Definition · number theory
IsPrimePow
{R : Type u_1} → [CommMonoidWithZero R] → R → Propn is a prime power if there is a prime p and a positive natural k such that n can be
written as p^k.
- Defined in
- Mathlib.Algebra.IsPrimePow
- Cited by
- 77 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
- Assumes
- CommMonoidWithZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommMonoidWithZerostatement and proof · cited by 913
- Primeproof · cited by 277
Cited by79
Results whose statement or proof uses this declaration.
- ArithmeticFunction.vonMangoldtproof · cited by 40
- isPrimePow_nat_iffstatement · cited by 9
- Nat.Primes.prodNatEquivstatement and proof · cited by 8
- IsPrimePow.ne_onestatement and proof · cited by 7
- ArithmeticFunction.vonMangoldt_nonnegproof · cited by 6
- Nat.Prime.isPrimePowstatement · cited by 5
- ArithmeticFunction.vonMangoldt_apply_oneproof · cited by 4
- ArithmeticFunction.vonMangoldt_apply_primeproof · cited by 4
- Prime.isPrimePowstatement · cited by 3
- not_isPrimePow_zerostatement · cited by 3
- ArithmeticFunction.vonMangoldt_ne_zero_iffstatement · cited by 3
- ArithmeticFunction.vonMangoldt_apply_powproof · cited by 3