bot_or_exists_ne_one — Mathlib

English

A subgroup is either trivial or contains a non-identity element.

Русский

Подгруппа либо тривиальна, либо содержит ненулевой элемент.

LaTeX

$$$$ H = \\bot \\;\\lor\\; \\exists x \\in H, x \\neq 1. $$$$

Lean4

/-- A subgroup is either the trivial subgroup or contains a non-identity element. -/
@[to_additive /-- A subgroup is either the trivial subgroup or contains a nonzero element. -/
    ]
theorem bot_or_exists_ne_one (H : Subgroup G) : H = ⊥ ∨ ∃ x ∈ H, x ≠ (1 : G) :=
  by
  convert H.bot_or_nontrivial
  rw [nontrivial_iff_exists_ne_one]

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