nontrivial_iff — Mathlib

English

A monoid M is nontrivial if and only if the associated submonoid of M is nontrivial; equivalently, Nontrivial M ⇔ Nontrivial Submonoid(M).

Русский

Моноид M не тривиален тогда и только тогда, когда соответствующий субмонод M не тривиален; не тривиальность M эквивалентна не тривиальности Submonoid(M).

LaTeX

$$$\mathrm{Nontrivial}(\mathrm{Submonoid} M) \iff \mathrm{Nontrivial}(M)$$$

Lean4

@[to_additive (attr := simp)]
theorem nontrivial_iff : Nontrivial (Submonoid M) ↔ Nontrivial M :=
  not_iff_not.mp ((not_nontrivial_iff_subsingleton.trans subsingleton_iff).trans not_nontrivial_iff_subsingleton.symm)

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