instNontrivialOfIsReduced — Mathlib

English

If K is a nontrivial reduced ring, then PerfectClosure(K,p) is nontrivial.

Русский

Если K — не тривиальное редуцированное кольцо, то PerfectClosure(K,p) также не тривиально.

LaTeX

$$$\text{Nontrivial}(\mathrm{PerfectClosure}(K,p)).$$$

Lean4

instance [CommRing K] [IsReduced K] (p : ℕ) [Fact p.Prime] [CharP K p] [Nontrivial K] : Nontrivial (PerfectClosure K p)
    where exists_pair_ne := ⟨0, 1, fun H => zero_ne_one ((eq_iff _ _ _ _).1 H)⟩

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