toPerfectRing — Mathlib

English

If K is a perfect field, then for any p, PerfectRing K p holds.

Русский

Если K — совершенное поле, то для любого p выполняется PerfectRing K p.

LaTeX

$$$ PerfectField K \Rightarrow (PerfectRing K p). $$$

Lean4

/-- A perfect field of characteristic `p` (prime) is a perfect ring. -/
instance toPerfectRing (p : ℕ) [hp : ExpChar K p] : PerfectRing K p :=
  by
  refine PerfectRing.ofSurjective _ _ fun y ↦ ?_
  rcases hp with _ | hp
  · simp [frobenius]
  rw [← not_forall_not]
  apply mt (X_pow_sub_C_irreducible_of_prime hp)
  apply mt separable_of_irreducible
  simp [separable_def, isCoprime_zero_right, isUnit_iff_degree_eq_zero, derivative_X_pow, degree_X_pow_sub_C hp.pos,
    hp.ne_zero]

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