bot_or_nontrivial — Mathlib

English

A subgroup is either the trivial subgroup or nontrivial.

Русский

Подгруппа либо тривиальна, либо не тривиальна.

LaTeX

$$$$ H = \\bot \\;\\lor\\; \\mathrm{Nontrivial}(H). $$$$

Lean4

/-- A subgroup is either the trivial subgroup or nontrivial. -/
@[to_additive /-- A subgroup is either the trivial subgroup or nontrivial. -/
    ]
theorem bot_or_nontrivial (H : Subgroup G) : H = ⊥ ∨ Nontrivial H :=
  by
  have := nontrivial_iff_ne_bot H
  tauto

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