unsym_mul — Mathlib

English

For a,b ∈ SymAlg(α), unsym(a * b) equals ⅟2 * (unsym(a) * unsym(b) + unsym(b) * unsym(a)).

Русский

Для a,b ∈ SymAlg(α) unsym(a * b) равно ⅟2 * (unsym(a) * unsym(b) + unsym(b) * unsym(a)).

LaTeX

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

Lean4

theorem unsym_mul [Mul α] [Add α] [One α] [OfNat α 2] [Invertible (2 : α)] (a b : αˢʸᵐ) :
    unsym (a * b) = ⅟2 * (unsym a * unsym b + unsym b * unsym a) :=
  rfl

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