English
Let G be a type and g1,g2 be two commutative group structures on G. If their multiplications coincide, then g1 = g2.
Русский
Пусть G — множество, и есть две структуры коммутативной группы на G, g1 и g2. Если их операции умножения совпадают, то g1 = g2.
LaTeX
$$$\\forall G\\,\\forall g_1,g_2\\in \\mathrm{CommGroup}(G),\\ (\\forall x,y\\in G:\\; x\\cdot_{g_1} y = x\\cdot_{g_2} y) \\Rightarrow g_1=g_2$$$
Lean4
@[to_additive (attr := ext)]
theorem ext {G : Type*} ⦃g₁ g₂ : CommGroup G⦄
(h_mul :
(letI := g₁;
HMul.hMul :
G → G → G) =
(letI := g₂;
HMul.hMul :
G → G → G)) :
g₁ = g₂ :=
CommGroup.toGroup_injective <| Group.ext h_mul
