instGroup — Mathlib

English

The coproduct G ∗ H is equipped with a group structure, with multiplication and inversion defined coherently with the constituent groups.

Русский

Копродукт G ∗ H снабжен структурой группы, умножение и обращение определены так, чтобы согласовываться с группами-составляющими.

LaTeX

$$$\text{instance } \text{Group }(G \ast H) \text{ with inv_mul_cancel defined by } mk\, inv\, x$ (details omitted).$$$

Lean4

@[to_additive]
instance : Group (G ∗ H) where inv_mul_cancel := mk_surjective.forall.2 fun x => mk_eq_mk.2 (con_inv_mul_cancel x)

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