English
In the symmetrized algebra SymAlg α, the product is given by a*b = sym( 1/2 · (unsym a · unsym b + unsym b · unsym a) ).
Русский
В симметризированной алгебре SymAlg α произведение элементов a и b определяется как a*b = sym( 1/2 · (unsym(a)·unsym(b) + unsym(b)·unsym(a)) ).
LaTeX
$$$ a * b \;=\; \\operatorname{sym}\\left( \\frac{1}{2} (\\operatorname{unsym}(a) \\cdot \\operatorname{unsym}(b) + \\operatorname{unsym}(b) \\cdot \\operatorname{unsym}(a)) \\right) $$$
Lean4
theorem mul_def [Add α] [Mul α] [One α] [OfNat α 2] [Invertible (2 : α)] (a b : αˢʸᵐ) :
a * b = sym (⅟2 * (unsym a * unsym b + unsym b * unsym a)) :=
rfl
