isZero_of_subsingleton — Mathlib

English

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

Русский

Если G — подмножество по коммутативной группе, то G является нулевым объектом в CommGrpCat.

LaTeX

$$$\forall G : \text{CommGrpCat}, [\text{Subsingleton } G.carrier] \Rightarrow \text{IsZero } G$$$

Lean4

@[to_additive]
theorem isZero_of_subsingleton (G : CommGrpCat) [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

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