Theorems · Theorem · nonassociative algebras

SymAlg.sym_mul_sym

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

Defined in

Mathlib.Algebra.Symmetrized

Cited by

1 results in Mathlib

Foundations

Depth 15 from the axioms · uses Quot.sound

Assumes

MulAddOneOfNatInvertible