Theorems · Theorem · commutative algebra
ExpChar.pow_prime_pow_mul_eq_one_iff
∀ {R : Type u_1} [inst : CommRing R] [IsReduced R] (p k m : ℕ) [ExpChar R p] (x : R), x ^ (p ^ k * m) = 1 ↔ x ^ m = 1- Defined in
- Mathlib.Algebra.CharP.Reduced
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- DFunLike.coeproof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- map_oneproof · cited by 861
- ExpCharstatement and proof · cited by 276
- IsReducedstatement and proof · cited by 98
- iterateFrobeniusproof · cited by 39
- pow_mul'proof · cited by 20
- iterateFrobenius_injproof · cited by 4
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.