subsingleton_quotient_top — Mathlib

English

If a quotient G/H is a singleton, then H = ⊤ in the subgroup lattice; equivalently, the subgroup is the whole group.

Русский

Если фактор-группа G/H теряет все элементы, то H = ⊤ в решётке подгрупп.

LaTeX

$$$H = \\top$ if $\\text{Quotient}(G,H)$ is singleton$$

Lean4

@[to_additive]
theorem subsingleton_quotient_top : Subsingleton (G ⧸ (⊤ : Subgroup G)) :=
  by
  dsimp [HasQuotient.Quotient, QuotientGroup.instHasQuotientSubgroup, Quotient]
  rw [leftRel_eq]
  exact Trunc.instSubsingletonTrunc

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