mathlib3 documentation

algebra.symmetrized

Symmetrized algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A commutative multiplication on a real or complex space can be constructed from any multiplication by "symmetrization" i.e $$ a \circ b = \frac{1}{2}(ab + ba) $$

We provide the symmetrized version of a type α as sym_alg α, with notation αˢʸᵐ.

Implementation notes #

The approach taken here is inspired by algebra.opposites. We use Oxford Spellings (IETF en-GB-oxendict).

References #

def sym_alg.sym {α : Type u_1} :

The element of sym_alg α that represents a : α.

Equations
def sym_alg.unsym {α : Type u_1} :

The element of α represented by x : αˢʸᵐ.

Equations
@[simp]
theorem sym_alg.unsym_sym {α : Type u_1} (a : α) :
@[simp]
theorem sym_alg.sym_unsym {α : Type u_1} (a : α) :
@[simp]
@[simp]
@[simp]
theorem sym_alg.sym_inj {α : Type u_1} {a b : α} :
@[simp]
theorem sym_alg.unsym_inj {α : Type u_1} {a b : αˢʸᵐ} :
@[protected, instance]
@[protected, instance]
def sym_alg.inhabited {α : Type u_1} [inhabited α] :
Equations
@[protected, instance]
@[protected, instance]
def sym_alg.unique {α : Type u_1} [unique α] :
Equations
@[protected, instance]
def sym_alg.is_empty {α : Type u_1} [is_empty α] :
@[protected, instance]
def sym_alg.has_zero {α : Type u_1} [has_zero α] :
Equations
@[protected, instance]
def sym_alg.has_one {α : Type u_1} [has_one α] :
Equations
@[protected, instance]
def sym_alg.has_add {α : Type u_1} [has_add α] :
Equations
@[protected, instance]
def sym_alg.has_sub {α : Type u_1} [has_sub α] :
Equations
@[protected, instance]
def sym_alg.has_neg {α : Type u_1} [has_neg α] :
Equations
@[protected, instance]
def sym_alg.has_mul {α : Type u_1} [has_add α] [has_mul α] [has_one α] [invertible 2] :
Equations
@[protected, instance]
def sym_alg.has_inv {α : Type u_1} [has_inv α] :
Equations
@[protected, instance]
def sym_alg.has_smul {α : Type u_1} (R : Type u_2) [has_smul R α] :
Equations
@[simp]
theorem sym_alg.sym_one {α : Type u_1} [has_one α] :
@[simp]
theorem sym_alg.sym_zero {α : Type u_1} [has_zero α] :
@[simp]
theorem sym_alg.unsym_one {α : Type u_1} [has_one α] :
@[simp]
theorem sym_alg.unsym_zero {α : Type u_1} [has_zero α] :
@[simp]
theorem sym_alg.sym_add {α : Type u_1} [has_add α] (a b : α) :
@[simp]
theorem sym_alg.unsym_add {α : Type u_1} [has_add α] (a b : αˢʸᵐ) :
@[simp]
theorem sym_alg.sym_sub {α : Type u_1} [has_sub α] (a b : α) :
@[simp]
theorem sym_alg.unsym_sub {α : Type u_1} [has_sub α] (a b : αˢʸᵐ) :
@[simp]
theorem sym_alg.sym_neg {α : Type u_1} [has_neg α] (a : α) :
@[simp]
theorem sym_alg.unsym_neg {α : Type u_1} [has_neg α] (a : αˢʸᵐ) :
theorem sym_alg.sym_mul_sym {α : Type u_1} [has_mul α] [has_add α] [has_one α] [invertible 2] (a b : α) :
@[simp]
theorem sym_alg.sym_inv {α : Type u_1} [has_inv α] (a : α) :
@[simp]
@[simp]
theorem sym_alg.sym_smul {α : Type u_1} {R : Type u_2} [has_smul R α] (c : R) (a : α) :
@[simp]
theorem sym_alg.unsym_smul {α : Type u_1} {R : Type u_2} [has_smul R α] (c : R) (a : αˢʸᵐ) :
@[simp]
theorem sym_alg.unsym_eq_one_iff {α : Type u_1} [has_one α] (a : αˢʸᵐ) :
@[simp]
theorem sym_alg.unsym_eq_zero_iff {α : Type u_1} [has_zero α] (a : αˢʸᵐ) :
@[simp]
theorem sym_alg.sym_eq_one_iff {α : Type u_1} [has_one α] (a : α) :
@[simp]
theorem sym_alg.sym_eq_zero_iff {α : Type u_1} [has_zero α] (a : α) :
theorem sym_alg.unsym_ne_one_iff {α : Type u_1} [has_one α] (a : αˢʸᵐ) :
theorem sym_alg.unsym_ne_zero_iff {α : Type u_1} [has_zero α] (a : αˢʸᵐ) :
theorem sym_alg.sym_ne_one_iff {α : Type u_1} [has_one α] (a : α) :
theorem sym_alg.sym_ne_zero_iff {α : Type u_1} [has_zero α] (a : α) :
@[protected, instance]
Equations
@[protected, instance]
def sym_alg.add_group {α : Type u_1} [add_group α] :
Equations
@[protected, instance]
def sym_alg.module {α : Type u_1} {R : Type u_2} [semiring R] [add_comm_monoid α] [module R α] :
Equations
@[protected, instance]
def sym_alg.sym.invertible {α : Type u_1} [has_mul α] [has_add α] [has_one α] [invertible 2] (a : α) [invertible a] :
Equations
@[simp]
theorem sym_alg.inv_of_sym {α : Type u_1} [has_mul α] [has_add α] [has_one α] [invertible 2] (a : α) [invertible a] :
@[protected, instance]
Equations
@[protected, instance]

The symmetrization of a real (unital, associative) algebra is a non-associative ring.

Equations

The squaring operation coincides for both multiplications

theorem sym_alg.sym_mul_self {α : Type u_1} [semiring α] [invertible 2] (a : α) :
theorem sym_alg.mul_comm {α : Type u_1} [has_mul α] [add_comm_semigroup α] [has_one α] [invertible 2] (a b : αˢʸᵐ) :
a * b = b * a
@[protected, instance]
Equations