Theorems · Theorem · commutative algebra
Prime.dvd_of_dvd_pow
∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p : M}, Prime p → ∀ {a : M} {n : ℕ}, p ∣ a ^ n → p ∣ a- Defined in
- Mathlib.Algebra.Prime.Defs
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext
- Assumes
- CommMonoidWithZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- IsUnitproof · cited by 1,602
- pow_zeroproof · cited by 1,094
- CommMonoidWithZerostatement and proof · cited by 913
- Primestatement and proof · cited by 277
- pow_succ'proof · cited by 228
- Prime.not_isUnitproof · cited by 29
- isUnit_of_dvd_oneproof · cited by 18
- Prime.dvd_or_dvdproof · cited by 17
Cited by14
Results whose statement or proof uses this declaration.
- Nat.Prime.dvd_of_dvd_powproof · cited by 15
- den_dvd_of_is_rootproof · cited by 2
- Associated.of_pow_associated_of_primeproof · cited by 2
- Int.emultiplicity_pow_sub_powproof · cited by 2
- UniqueFactorizationMonoid.prime_pow_coprime_prod_of_coprime_insertproof · cited by 2
- Prime.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvdproof · cited by 2
- Ideal.finprod_not_dvdproof · cited by 1
- not_dvd_geom_sum₂proof · cited by 1
- emultiplicity_geom_sum₂_eq_oneproof · cited by 1
- Prime.isRadicalproof · cited by 1
- emultiplicity_pow_prime_pow_sub_pow_prime_powproof · cited by 1
- dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLTproof · cited by 1