Results about characteristic p reduced rings

theorem frobenius_inj (R : Type u_1) [CommRing R] [IsReduced R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] : Function.Injective ⇑(frobenius R p)

theorem isSquare_of_charTwo' {R : Type u_1} [Finite R] [CommRing R] [IsReduced R] [CharP R 2] (a : R) : IsSquare a

If ringChar R = 2, where R is a finite reduced commutative ring, then every a : R is a square.

@[simp]

theorem CharP.pow_prime_pow_mul_eq_one_iff {R : Type u_1} [CommRing R] [IsReduced R] (p : ℕ) (k : ℕ) (m : ℕ) [Fact (Nat.Prime p)] [CharP R p] (x : R) : x ^ (p ^ k * m) = 1 ↔ x ^ m = 1