instNontrivial — Mathlib

English

If α is a nontrivial semiring, then the lattice of ideals is nontrivial; in particular there exists an ideal different from ⊤.

Русский

Если α не тривиален, множество идеалов не тривиально; существует идеал, отличный от ⊤.

LaTeX

$$$[Nontrivial\; \alpha] \Rightarrow \exists I:\ Ideal\ α, I \neq \top$$$

Lean4

instance [Nontrivial α] : Nontrivial (Ideal α) :=
  by
  rcases @exists_maximal α _ _ with ⟨M, hM, _⟩
  exact nontrivial_of_ne M ⊤ hM

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