bot_or_exists_ne_one — Mathlib

English

A submonoid is either the bottom submonoid or contains a non-identity element.

Русский

Подмножество либо равно ⊥, либо содержит элемент, не равный единице.

LaTeX

$$$ \text{bot\_or\_exists\_ne\_one} (S) : S = \bot \lor \exists x \in S, x \neq 1_M$$$

Lean4

/-- A submonoid is either the trivial submonoid or contains a nonzero element. -/
@[to_additive /-- An additive submonoid is either the trivial additive submonoid or contains a nonzero
      element. -/
    ]
theorem bot_or_exists_ne_one (S : Submonoid M) : S = ⊥ ∨ ∃ x ∈ S, x ≠ (1 : M) :=
  S.bot_or_nontrivial.imp_right S.nontrivial_iff_exists_ne_one.mp

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