isSquare_of_charTwo'
theorem isSquare_of_charTwo' :
∀ {R : Type u_1} [inst : Finite R] [inst : CommRing R] [inst_1 : IsReduced R] [inst_2 : CharP R 2] (a : R),
IsSquare a
The theorem `isSquare_of_charTwo'` states that for any type `R` that has instances of being a finite, commutative ring that is reduced, and has a characteristic of 2, every element `a` of `R` satisfies the property of being a square. In other words, if `R` is a finite, reduced commutative ring with characteristic 2, then for any `a` in `R`, there exists an `r` in `R` such that `a = r * r`.
More concisely: In a finite, reduced commutative ring R with characteristic 2, every element is a square.
|
frobenius_inj
theorem frobenius_inj :
∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsReduced R] (p : ℕ) [inst_2 : ExpChar R p],
Function.Injective ⇑(frobenius R p)
The theorem `frobenius_inj` states that for any type `R` which is a commutative ring and is reduced, and for any natural number `p` such that `R` has characteristic `p`, the Frobenius map that sends each element `x` in `R` to `x^p` is injective. This means that if `x^p = y^p` for some `x` and `y` in `R`, then `x = y`.
More concisely: In a commutative, reduced ring `R` of characteristic `p`, the `p`-th power map is an injective homomorphism.
|