instNontrivial — Mathlib

English

If R is nontrivial, then RingCon R is nontrivial as a lattice-ordered structure.

Русский

Если R не тривиально, то RingCon R не тривиально как структура решетки.

LaTeX

$$$$ \text{Nontrivial}(R) \Rightarrow \text{Nontrivial}(RingCon(R)) $$$$

Lean4

instance [Nontrivial R] : Nontrivial (RingCon R) where
  exists_pair_ne :=
    let ⟨x, y, ne⟩ := exists_pair_ne R
    ⟨⊥, ⊤, ne_of_apply_ne (· x y) <| by simp [ne]⟩

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