Theorems · Theorem · nonassociative algebras

SymAlg.mul_def

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

Defined in

Mathlib.Algebra.Symmetrized

Cited by

2 results in Mathlib

Foundations

Depth 15 from the axioms · uses Quot.sound

Assumes

AddMulOneOfNatInvertible