instBot — Mathlib

English

The trivial subgroup of G is the subgroup consisting of the identity element.

Русский

Тривиальная подгруппа G состоит только из единицы.

LaTeX

$$$$ (\\bot : \\mathrm{Subgroup}(G)) = \\{1\\} \\quad\\text{(as a subgroup).} $$$$

Lean4

/-- The trivial subgroup `{1}` of a group `G`. -/
@[to_additive /-- The trivial `AddSubgroup` `{0}` of an `AddGroup` `G`. -/
    ]
instance : Bot (Subgroup G) :=
  ⟨{ (⊥ : Submonoid G) with inv_mem' := by simp }⟩

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