isZero_of_subsingleton — Mathlib

English

If G is a subsingleton group, then G is a zero object in GrpCat.

Русский

Если G является одиночной группой, то она нулевой объект в GrpCat.

LaTeX

$$$[\text{Subsingleton } G] \Rightarrow \text{IsZero } G$$$

Lean4

@[to_additive]
theorem isZero_of_subsingleton (G : GrpCat) [Subsingleton G] : IsZero G :=
  by
  refine ⟨fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩⟩
  · ext x
    have : x = 1 := Subsingleton.elim _ _
    rw [this, map_one, map_one]
  · ext
    subsingleton

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