toGroup_injective — Mathlib

English

The forgetful map from commutative groups to groups is injective: two commutative group structures with the same underlying group are equal.

Русский

Функция забывания из коммутативных групп в группы инъективна: две структуры коммутативной группы, имеющие одинаковые виходящие группы, равны.

LaTeX

$$$\\forall G\\,\\forall \\mathcal{G}_1,\\mathcal{G}_2\\in \\mathrm{CommGroup}(G),\\ \\mathrm{toGroup}(\\mathcal{G}_1)=\\mathrm{toGroup}(\\mathcal{G}_2) \\Rightarrow \\mathcal{G}_1=\\mathcal{G}_2$$$

Lean4

@[to_additive]
theorem toGroup_injective {G : Type*} : Injective (@CommGroup.toGroup G) := by rintro ⟨⟩ ⟨⟩ ⟨⟩; rfl

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