instMulOfAddOfInvertibleOfNat — Mathlib

English

There is a multiplication on SymAlg(α) defined by a * b = sym(⅟2 * (unsym(a) * unsym(b) + unsym(b) * unsym(a))).

Русский

Существует умножение на SymAlg(α), заданное формулой a * b = sym(⅟2 · (unsym(a) unsym(b) + unsym(b) unsym(a))).

LaTeX

$$$a \\cdot b = \\operatorname{sym}\\left(\\tfrac{1}{2}\\left(\\operatorname{unsym}(a)\\operatorname{unsym}(b) + \\operatorname{unsym}(b)\\operatorname{unsym}(a)\\right)\\right).$$$

Lean4

instance [Add α] [Mul α] [One α] [OfNat α 2] [Invertible (2 : α)] : Mul αˢʸᵐ where
  mul a b := sym (⅟2 * (unsym a * unsym b + unsym b * unsym a))

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