# mathlib3documentation

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 (α : Type u_1) :
Type u_1

The symmetrized algebra has the same underlying space as the original algebra.

Equations
Instances for sym_alg
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]
theorem sym_alg.sym_comp_unsym {α : Type u_1} :
@[simp]
theorem sym_alg.unsym_comp_sym {α : Type u_1} :
@[simp]
theorem sym_alg.sym_symm {α : Type u_1} :
@[simp]
theorem sym_alg.unsym_symm {α : Type u_1} :
theorem sym_alg.sym_bijective {α : Type u_1} :
theorem sym_alg.unsym_bijective {α : Type u_1} :
theorem sym_alg.sym_injective {α : Type u_1} :
theorem sym_alg.sym_surjective {α : Type u_1} :
theorem sym_alg.unsym_injective {α : Type u_1} :
theorem sym_alg.unsym_surjective {α : Type u_1} :
@[simp]
theorem sym_alg.sym_inj {α : Type u_1} {a b : α} :
a = b
@[simp]
theorem sym_alg.unsym_inj {α : Type u_1} {a b : αˢʸᵐ} :
a = b
@[protected, instance]
def sym_alg.nontrivial {α : Type u_1} [nontrivial α] :
@[protected, instance]
def sym_alg.inhabited {α : Type u_1} [inhabited α] :
Equations
@[protected, instance]
def sym_alg.subsingleton {α : Type u_1} [subsingleton α] :
@[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]
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) [ α] :
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.mul_def {α : Type u_1} [has_add α] [has_mul α] [has_one α] [invertible 2] (a b : αˢʸᵐ) :
theorem sym_alg.unsym_mul {α : Type u_1} [has_mul α] [has_add α] [has_one α] [invertible 2] (a b : αˢʸᵐ) :
theorem sym_alg.sym_mul_sym {α : Type u_1} [has_mul α] [has_add α] [has_one α] [invertible 2] (a b : α) :
= sym_alg.sym ( 2 * (a * b + b * a))
@[simp]
theorem sym_alg.sym_inv {α : Type u_1} [has_inv α] (a : α) :
@[simp]
theorem sym_alg.unsym_inv {α : Type u_1} [has_inv α] (a : αˢʸᵐ) :
@[simp]
theorem sym_alg.sym_smul {α : Type u_1} {R : Type u_2} [ α] (c : R) (a : α) :
@[simp]
theorem sym_alg.unsym_smul {α : Type u_1} {R : Type u_2} [ α] (c : R) (a : αˢʸᵐ) :
@[simp]
theorem sym_alg.unsym_eq_one_iff {α : Type u_1} [has_one α] (a : αˢʸᵐ) :
a = 1
@[simp]
theorem sym_alg.unsym_eq_zero_iff {α : Type u_1} [has_zero α] (a : αˢʸᵐ) :
a = 0
@[simp]
theorem sym_alg.sym_eq_one_iff {α : Type u_1} [has_one α] (a : α) :
a = 1
@[simp]
theorem sym_alg.sym_eq_zero_iff {α : Type u_1} [has_zero α] (a : α) :
a = 0
theorem sym_alg.unsym_ne_one_iff {α : Type u_1} [has_one α] (a : αˢʸᵐ) :
a 1
theorem sym_alg.unsym_ne_zero_iff {α : Type u_1} [has_zero α] (a : αˢʸᵐ) :
a 0
theorem sym_alg.sym_ne_one_iff {α : Type u_1} [has_one α] (a : α) :
a 1
theorem sym_alg.sym_ne_zero_iff {α : Type u_1} [has_zero α] (a : α) :
a 0
@[protected, instance]
def sym_alg.add_comm_semigroup {α : Type u_1}  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def sym_alg.add_comm_monoid {α : Type u_1}  :
Equations
@[protected, instance]
def sym_alg.add_comm_group {α : Type u_1}  :
Equations
@[protected, instance]
def sym_alg.module {α : Type u_1} {R : Type u_2} [semiring 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]
def sym_alg.non_assoc_semiring {α : Type u_1} [semiring α] [invertible 2] :
Equations
@[protected, instance]
def sym_alg.non_assoc_ring {α : Type u_1} [ring α] [invertible 2] :

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

Equations

The squaring operation coincides for both multiplications

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