mathlib3 documentation

algebra.star.self_adjoint

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

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

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.all {R : Type u_1} [has_star R] [has_trivial_star R] (r : R) :

All elements are self-adjoint when star is trivial.

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} :
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_monoid 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.conjugate {R : Type u_1} [semigroup R] [star_semigroup R] {x : R} (hx : is_self_adjoint x) (z : R) :
theorem is_self_adjoint.conjugate' {R : Type u_1} [semigroup R] [star_semigroup R] {x : R} (hx : is_self_adjoint x) (z : R) :
theorem is_self_adjoint.pow {R : Type u_1} [monoid R] [star_semigroup R] {x : R} (hx : is_self_adjoint x) (n : ) :
theorem is_self_adjoint.bit1 {R : Type u_1} [semiring R] [star_ring R] {x : R} (hx : is_self_adjoint x) :
@[simp]
theorem is_self_adjoint_nat_cast {R : Type u_1} [semiring R] [star_ring R] (n : ) :
theorem is_self_adjoint.mul {R : Type u_1} [comm_semigroup R] [star_semigroup R] {x y : R} (hx : is_self_adjoint x) (hy : is_self_adjoint y) :
@[simp]
theorem is_self_adjoint_int_cast {R : Type u_1} [ring R] [star_ring R] (z : ) :
theorem is_self_adjoint.zpow {R : Type u_1} [division_semiring R] [star_ring R] {x : R} (hx : is_self_adjoint x) (n : ) :
theorem is_self_adjoint.div {R : Type u_1} [semifield R] [star_ring R] {x y : R} (hx : is_self_adjoint x) (hy : is_self_adjoint y) :
theorem is_self_adjoint.smul {R : Type u_1} {A : Type u_2} [has_star R] [add_monoid A] [star_add_monoid A] [has_smul R A] [star_module R A] {r : R} (hr : is_self_adjoint r) {x : A} (hx : is_self_adjoint x) :

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

Equations
Instances for skew_adjoint
@[simp, norm_cast]
@[protected, instance]
Equations
@[protected, instance]
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]
Equations
@[simp, norm_cast]
theorem self_adjoint.coe_inv {R : Type u_1} [field R] [star_ring R] (x : (self_adjoint R)) :
@[protected, instance]
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]
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]
Equations
@[protected, instance]
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]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[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]
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]
Equations
theorem is_self_adjoint.smul_mem_skew_adjoint {R : Type u_1} {A : Type u_2} [ring R] [add_comm_group A] [module R A] [star_add_monoid R] [star_add_monoid A] [star_module R A] {r : R} (hr : r skew_adjoint R) {a : A} (ha : is_self_adjoint a) :

Scalar multiplication of a self-adjoint element by a skew-adjoint element produces a skew-adjoint element.

theorem is_self_adjoint_smul_of_mem_skew_adjoint {R : Type u_1} {A : Type u_2} [ring R] [add_comm_group A] [module R A] [star_add_monoid R] [star_add_monoid A] [star_module R A] {r : R} (hr : r skew_adjoint R) {a : A} (ha : a skew_adjoint A) :

Scalar multiplication of a skew-adjoint element by a skew-adjoint element produces a self-adjoint element.

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]