isSquare_of_charTwo' — Mathlib

English

If the ring is finite, reduced, and has characteristic 2, then every element is a square.

Русский

Если кольцо конечное и редуцируемое с характеристикой 2, то любой элемент является квадратом.

LaTeX

$$$\\forall a\\in R\\,\\exists b\\in R\\; (b^2 = a)$$$

Lean4

/-- If `ringChar R = 2`, where `R` is a finite reduced commutative ring,
then every `a : R` is a square. -/
theorem isSquare_of_charTwo' {R : Type*} [Finite R] [CommRing R] [IsReduced R] [CharP R 2] (a : R) : IsSquare a :=
  by
  cases nonempty_fintype R
  exact
    Exists.imp (fun b h => pow_two b ▸ Eq.symm h)
      (((Fintype.bijective_iff_injective_and_card _).mpr ⟨frobenius_inj R 2, rfl⟩).surjective a)

Похожие утверждения