Theorems · Theorem · nonassociative algebras

SymAlg.unsym_mul

∀ {α : Type u_1} [inst : Mul α] [inst_1 : Add α] [inst_2 : One α] [inst_3 : OfNat α 2] [inst_4 : Invertible 2]
  (a b : αˢʸᵐ), SymAlg.unsym (a * b) = ⅟2 * (SymAlg.unsym a * SymAlg.unsym b + SymAlg.unsym b * SymAlg.unsym a)

Defined in

Mathlib.Algebra.Symmetrized

Cited by

0 results in Mathlib

Foundations

Depth 15 from the axioms · uses Quot.sound

Assumes

MulAddOneOfNatInvertible