sym_mul_sym — Mathlib

English

In α, the product of two symmetrized elements satisfies sym a · sym b = sym(⅟2 · (a b + b a)).

Русский

В α произведение двух симметрированных элементов удовлетворяет sym a · sym b = sym(⅟2 · (a b + b a)).

LaTeX

$$$\forall a,b \in \alpha,\ sym a \cdot \sym b = \operatorname{sym}\left(\tfrac{1}{2}(a b + b a)\right)$$$

Lean4

theorem sym_mul_sym [Mul α] [Add α] [One α] [OfNat α 2] [Invertible (2 : α)] (a b : α) :
    sym a * sym b = sym (⅟2 * (a * b + b * a)) :=
  rfl

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