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 is_self_adjoint {R : Type u_1} [has_star R] (x : R) :
Prop

An element is self-adjoint if it is equal to its star.

Equations
@[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 is_self_adjoint.star_eq {R : Type u_1} [has_star R] {x : R} (hx : is_self_adjoint x) :
theorem is_self_adjoint_iff {R : Type u_1} [has_star R] {x : R} :
@[simp]
theorem is_self_adjoint.star_mul_self {R : Type u_1} [semigroup R] [star_semigroup R] (x : R) :
@[simp]
theorem is_self_adjoint.mul_star_self {R : Type u_1} [semigroup R] [star_semigroup R] (x : R) :
theorem is_self_adjoint.star_hom_apply {F : Type u_1} {R : Type u_2} {S : Type u_3} [has_star R] [has_star S] [star_hom_class F R S] {x : R} (hx : is_self_adjoint x) (f : F) :

Functions in a star_hom_class preserve self-adjoint elements.

theorem is_self_adjoint.add {R : Type u_1} [add_group R] [star_add_monoid R] {x y : R} (hx : is_self_adjoint x) (hy : is_self_adjoint y) :
theorem is_self_adjoint.neg {R : Type u_1} [add_group R] [star_add_monoid R] {x : R} (hx : is_self_adjoint x) :
theorem is_self_adjoint.sub {R : Type u_1} [add_group R] [star_add_monoid R] {x y : R} (hx : is_self_adjoint x) (hy : is_self_adjoint y) :
theorem is_self_adjoint.bit0 {R : Type u_1} [add_group R] [star_add_monoid R] {x : R} (hx : is_self_adjoint x) :
theorem is_self_adjoint.conjugate {R : Type u_1} [non_unital_semiring R] [star_ring R] {x : R} (hx : is_self_adjoint x) (z : R) :
theorem is_self_adjoint.conjugate' {R : Type u_1} [non_unital_semiring R] [star_ring R] {x : R} (hx : is_self_adjoint x) (z : R) :
theorem is_self_adjoint_one (R : Type u_1) [ring R] [star_ring R] :
theorem is_self_adjoint.bit1 {R : Type u_1} [ring R] [star_ring R] {x : R} (hx : is_self_adjoint x) :
theorem is_self_adjoint.pow {R : Type u_1} [ring R] [star_ring R] {x : R} (hx : is_self_adjoint x) (n : ) :
theorem is_self_adjoint.mul {R : Type u_1} [non_unital_comm_ring R] [star_ring R] {x y : R} (hx : is_self_adjoint x) (hy : is_self_adjoint y) :
theorem is_self_adjoint.inv {R : Type u_1} [field R] [star_ring R] {x : R} (hx : is_self_adjoint x) :
theorem is_self_adjoint.div {R : Type u_1} [field R] [star_ring R] {x y : R} (hx : is_self_adjoint x) (hy : is_self_adjoint y) :
theorem is_self_adjoint.zpow {R : Type u_1} [field R] [star_ring R] {x : R} (hx : is_self_adjoint x) (n : ) :
theorem is_self_adjoint.smul {R : Type u_1} {A : Type u_2} [has_star R] [has_trivial_star R] [add_group A] [star_add_monoid A] [has_smul R A] [star_module R A] (r : R) {x : A} (hx : is_self_adjoint x) :
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
theorem self_adjoint.mem_iff {R : Type u_1} [add_group R] [star_add_monoid R] {x : R} :
@[simp, norm_cast]
@[protected, instance]
Equations
@[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]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[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]
Equations
@[simp, norm_cast]
theorem self_adjoint.coe_mul {R : Type u_1} [non_unital_comm_ring R] [star_ring R] (x y : (self_adjoint R)) :
(x * y) = x * y
@[protected, instance]
Equations
  • self_adjoint.comm_ring = function.injective.comm_ring coe self_adjoint.comm_ring._proof_1 self_adjoint.comm_ring._proof_2 self_adjoint.comm_ring._proof_3 self_adjoint.comm_ring._proof_4 self_adjoint.comm_ring._proof_5 self_adjoint.comm_ring._proof_6 self_adjoint.comm_ring._proof_7 self_adjoint.comm_ring._proof_8 self_adjoint.comm_ring._proof_9 self_adjoint.comm_ring._proof_10 self_adjoint.comm_ring._proof_11 self_adjoint.comm_ring._proof_12
@[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
theorem self_adjoint.rat_cast_mem {R : Type u_1} [field R] [star_ring R] (x : ) :
@[protected, instance]
Equations
@[simp, norm_cast]
theorem self_adjoint.coe_rat_cast {R : Type u_1} [field R] [star_ring R] (x : ) :
@[protected, instance]
Equations
@[simp, norm_cast]
theorem self_adjoint.coe_rat_smul {R : Type u_1} [field R] [star_ring R] (x : (self_adjoint R)) (a : ) :
(a x) = a x
@[protected, instance]
def self_adjoint.field {R : Type u_1} [field R] [star_ring R] :
Equations
@[protected, instance]
def self_adjoint.has_smul {R : Type u_1} {A : Type u_2} [has_star R] [has_trivial_star R] [add_group A] [star_add_monoid A] [has_smul 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_smul 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} :