mathlib documentation

algebra.star.self_adjoint

Self-adjoint, skew-adjoint and normal elements of a star additive group #

This file defines self_adjoint R (resp. skew_adjoint R), where R is a star additive group, as the additive subgroup containing the elements that satisfy star x = x (resp. star x = -x). This includes, for instance, (skew-)Hermitian operators on Hilbert spaces.

We also define is_star_normal R, a Prop that states that an element x satisfies star x * x = x * star x.

Implementation notes #

TODO #

def skew_adjoint (R : Type u_1) [add_comm_group R] [star_add_monoid R] :

The skew-adjoint elements of a star additive group, as an additive subgroup.

Equations
Instances for skew_adjoint
@[class]
structure is_star_normal {R : Type u_1} [has_mul R] [has_star R] (x : R) :
Prop

An element of a star monoid is normal if it commutes with its adjoint.

Instances of this typeclass
theorem star_comm_self' {R : Type u_1} [has_mul R] [has_star R] (x : R) [is_star_normal x] :
theorem self_adjoint.mem_iff {R : Type u_1} [add_group R] [star_add_monoid R] {x : R} :
@[simp, norm_cast]
@[protected, instance]
Equations
theorem self_adjoint.bit0_mem {R : Type u_1} [add_group R] [star_add_monoid R] {x : R} (hx : x self_adjoint R) :
@[protected, instance]
def self_adjoint.has_one {R : Type u_1} [ring R] [star_ring R] :
Equations
@[simp, norm_cast]
theorem self_adjoint.coe_one {R : Type u_1} [ring R] [star_ring R] :
1 = 1
@[protected, instance]
theorem self_adjoint.one_mem {R : Type u_1} [ring R] [star_ring R] :
theorem self_adjoint.bit1_mem {R : Type u_1} [ring R] [star_ring R] {x : R} (hx : x self_adjoint R) :
theorem self_adjoint.conjugate {R : Type u_1} [ring R] [star_ring R] {x : R} (hx : x self_adjoint R) (z : R) :
theorem self_adjoint.conjugate' {R : Type u_1} [ring R] [star_ring R] {x : R} (hx : x self_adjoint R) (z : R) :
theorem self_adjoint.is_star_normal_of_mem {R : Type u_1} [ring R] [star_ring R] {x : R} (hx : x self_adjoint R) :
@[protected, instance]
def self_adjoint.is_star_normal {R : Type u_1} [ring R] [star_ring R] (x : (self_adjoint R)) :
@[protected, instance]
Equations
@[simp, norm_cast]
theorem self_adjoint.coe_pow {R : Type u_1} [ring R] [star_ring R] (x : (self_adjoint R)) (n : ) :
(x ^ n) = x ^ n
@[protected, instance]
def self_adjoint.has_mul {R : Type u_1} [comm_ring R] [star_ring R] :
Equations
@[simp, norm_cast]
theorem self_adjoint.coe_mul {R : Type u_1} [comm_ring R] [star_ring R] (x y : (self_adjoint R)) :
(x * y) = x * y
@[protected, instance]
Equations
@[protected, instance]
def self_adjoint.has_inv {R : Type u_1} [field R] [star_ring R] :
Equations
@[simp, norm_cast]
theorem self_adjoint.coe_inv {R : Type u_1} [field R] [star_ring R] (x : (self_adjoint R)) :
@[protected, instance]
def self_adjoint.has_div {R : Type u_1} [field R] [star_ring R] :
Equations
@[simp, norm_cast]
theorem self_adjoint.coe_div {R : Type u_1} [field R] [star_ring R] (x y : (self_adjoint R)) :
(x / y) = x / y
@[protected, instance]
Equations
@[simp, norm_cast]
theorem self_adjoint.coe_zpow {R : Type u_1} [field R] [star_ring R] (x : (self_adjoint R)) (z : ) :
(x ^ z) = x ^ z
@[protected, instance]
def self_adjoint.field {R : Type u_1} [field R] [star_ring R] :
Equations
theorem self_adjoint.smul_mem {R : Type u_1} {A : Type u_2} [has_star R] [has_trivial_star R] [add_group A] [star_add_monoid A] [has_scalar R A] [star_module R A] (r : R) {x : A} (h : x self_adjoint A) :
@[protected, instance]
def self_adjoint.has_scalar {R : Type u_1} {A : Type u_2} [has_star R] [has_trivial_star R] [add_group A] [star_add_monoid A] [has_scalar R A] [star_module R A] :
Equations
@[simp, norm_cast]
theorem self_adjoint.coe_smul {R : Type u_1} {A : Type u_2} [has_star R] [has_trivial_star R] [add_group A] [star_add_monoid A] [has_scalar R A] [star_module R A] (r : R) (x : (self_adjoint A)) :
(r x) = r x
@[protected, instance]
def self_adjoint.mul_action {R : Type u_1} {A : Type u_2} [has_star R] [has_trivial_star R] [add_group A] [star_add_monoid A] [monoid R] [mul_action R A] [star_module R A] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def self_adjoint.module {R : Type u_1} {A : Type u_2} [has_star R] [has_trivial_star R] [add_comm_group A] [star_add_monoid A] [semiring R] [module R A] [star_module R A] :
Equations
theorem skew_adjoint.mem_iff {R : Type u_1} [add_comm_group R] [star_add_monoid R] {x : R} :
@[simp, norm_cast]
@[protected, instance]
Equations
theorem skew_adjoint.bit0_mem {R : Type u_1} [add_comm_group R] [star_add_monoid R] {x : R} (hx : x skew_adjoint R) :
theorem skew_adjoint.conjugate {R : Type u_1} [ring R] [star_ring R] {x : R} (hx : x skew_adjoint R) (z : R) :
theorem skew_adjoint.conjugate' {R : Type u_1} [ring R] [star_ring R] {x : R} (hx : x skew_adjoint R) (z : R) :
theorem skew_adjoint.is_star_normal_of_mem {R : Type u_1} [ring R] [star_ring R] {x : R} (hx : x skew_adjoint R) :
@[protected, instance]
def skew_adjoint.is_star_normal {R : Type u_1} [ring R] [star_ring R] (x : (skew_adjoint R)) :
theorem skew_adjoint.smul_mem {R : Type u_1} {A : Type u_2} [has_star R] [has_trivial_star R] [add_comm_group A] [star_add_monoid A] [monoid R] [distrib_mul_action R A] [star_module R A] (r : R) {x : A} (h : x skew_adjoint A) :
@[protected, instance]
Equations
@[simp, norm_cast]
theorem skew_adjoint.coe_smul {R : Type u_1} {A : Type u_2} [has_star R] [has_trivial_star R] [add_comm_group A] [star_add_monoid A] [monoid R] [distrib_mul_action R A] [star_module R A] (r : R) (x : (skew_adjoint A)) :
(r x) = r x
@[protected, instance]
def skew_adjoint.module {R : Type u_1} {A : Type u_2} [has_star R] [has_trivial_star R] [add_comm_group A] [star_add_monoid A] [semiring R] [module R A] [star_module R A] :
Equations
@[protected, instance]
def is_star_normal_zero {R : Type u_1} [semiring R] [star_ring R] :
@[protected, instance]
def is_star_normal_one {R : Type u_1} [monoid R] [star_semigroup R] :
@[protected, instance]
@[protected, instance]
@[protected, instance]
def comm_monoid.is_star_normal {R : Type u_1} [comm_monoid R] [star_semigroup R] {x : R} :