mk_of_inv_mul — Mathlib

English

In the free product of G and H, for every x in G ⊕ H, the element mk(of (x.map inv inv)) · mk(of x) equals 1.

Русский

В свободном произведении G и H для каждого x ∈ G ⊕ H выполняется: mk(of(совпадение x со значениями inv inv)) · mk(of x) = 1.

LaTeX

$$$ \forall x : G \oplus H,\; \operatorname{mk}(\operatorname{of}(x_{\mapsto} Inv.inv, x_{\mapsto} Inv.inv)) \cdot \operatorname{mk}(\operatorname{of} x) = 1. $$$

Lean4

@[to_additive]
theorem mk_of_inv_mul : ∀ x : G ⊕ H, mk (of (x.map Inv.inv Inv.inv)) * mk (of x) = 1
  | Sum.inl _ => map_mul_eq_one inl (inv_mul_cancel _)
  | Sum.inr _ => map_mul_eq_one inr (inv_mul_cancel _)

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