# mathlib3documentation

analysis.normed_space.star.basic

# Normed star rings and algebras #

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

A normed star group is a normed group with a compatible star which is isometric.

A C⋆-ring is a normed star group that is also a ring and that verifies the stronger condition ‖x⋆ * x‖ = ‖x‖^2 for all x. If a C⋆-ring is also a star algebra, then it is a C⋆-algebra.

To get a C⋆-algebra E over field 𝕜, use [normed_field 𝕜] [star_ring 𝕜] [normed_ring E] [star_ring E] [cstar_ring E] [normed_algebra 𝕜 E] [star_module 𝕜 E].

## TODO #

• Show that ‖x⋆ * x‖ = ‖x‖^2 is equivalent to ‖x⋆ * x‖ = ‖x⋆‖ * ‖x‖, which is used as the definition of C*-algebras in some sources (e.g. Wikipedia).
@[class]
structure normed_star_group (E : Type u_1)  :
Prop
• norm_star : (x : E),

A normed star group is a normed group with a compatible star which is isometric.

Instances of this typeclass
@[simp]
theorem nnnorm_star {E : Type u_2} (x : E) :
def star_normed_add_group_hom {E : Type u_2}  :

The star map in a normed star group is a normed group homomorphism.

Equations
theorem star_isometry {E : Type u_2}  :

The star map in a normed star group is an isometry

@[protected, instance]
@[protected, instance]
@[class]
structure cstar_ring (E : Type u_4) [star_ring E] :
Prop

A C*-ring is a normed star ring that satifies the stronger condition ‖x⋆ * x‖ = ‖x‖^2 for every x.

Instances of this typeclass
@[protected, instance]
@[protected, instance]

In a C*-ring, star preserves the norm.

theorem cstar_ring.norm_star_mul_self' {E : Type u_2} [star_ring E] [cstar_ring E] {x : E} :
@[simp]
theorem cstar_ring.star_mul_self_eq_zero_iff {E : Type u_2} [star_ring E] [cstar_ring E] (x : E) :
= 0 x = 0
theorem cstar_ring.star_mul_self_ne_zero_iff {E : Type u_2} [star_ring E] [cstar_ring E] (x : E) :
0 x 0
@[simp]
theorem cstar_ring.mul_star_self_eq_zero_iff {E : Type u_2} [star_ring E] [cstar_ring E] (x : E) :
= 0 x = 0
theorem cstar_ring.mul_star_self_ne_zero_iff {E : Type u_2} [star_ring E] [cstar_ring E] (x : E) :
0 x 0
@[protected, instance]
def pi.star_ring' {ι : Type u_4} {R : ι Type u_7} [Π (i : ι), ] [Π (i : ι), star_ring (R i)] :
star_ring (Π (i : ι), R i)

This instance exists to short circuit type class resolution because of problems with inference involving Π-types.

Equations
@[protected, instance]
def prod.cstar_ring {R₁ : Type u_5} {R₂ : Type u_6} [star_ring R₁] [cstar_ring R₁] [star_ring R₂] [cstar_ring R₂] :
cstar_ring (R₁ × R₂)
@[protected, instance]
def pi.cstar_ring {ι : Type u_4} {R : ι Type u_7} [Π (i : ι), ] [Π (i : ι), star_ring (R i)] [fintype ι] [ (i : ι), cstar_ring (R i)] :
cstar_ring (Π (i : ι), R i)
@[protected, instance]
def pi.cstar_ring' {ι : Type u_4} {R₁ : Type u_5} [star_ring R₁] [cstar_ring R₁] [fintype ι] :
cstar_ring R₁)
@[simp]
theorem cstar_ring.norm_one {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] [nontrivial E] :
@[protected, instance]
@[simp]
theorem cstar_ring.norm_of_mem_unitary {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] [nontrivial E] {U : E} (hU : U ) :
@[simp]
theorem cstar_ring.norm_coe_unitary_mul {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] (U : (unitary E)) (A : E) :
@[simp]
theorem cstar_ring.norm_unitary_smul {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] (U : (unitary E)) (A : E) :
theorem cstar_ring.norm_mem_unitary_mul {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] {U : E} (A : E) (hU : U ) :
@[simp]
theorem cstar_ring.norm_mul_coe_unitary {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] (A : E) (U : (unitary E)) :
theorem cstar_ring.norm_mul_mem_unitary {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] (A : E) {U : E} (hU : U ) :
theorem is_self_adjoint.nnnorm_pow_two_pow {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] {x : E} (hx : is_self_adjoint x) (n : ) :
x ^ 2 ^ n‖₊ = x‖₊ ^ 2 ^ n
theorem self_adjoint.nnnorm_pow_two_pow {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] (x : (self_adjoint E)) (n : ) :
x ^ 2 ^ n‖₊ = x‖₊ ^ 2 ^ n
def starₗᵢ (𝕜 : Type u_1) {E : Type u_2} [star_ring 𝕜] [ E] [ E] :

star bundled as a linear isometric equivalence

Equations
@[simp]
theorem coe_starₗᵢ {𝕜 : Type u_1} {E : Type u_2} [star_ring 𝕜] [ E] [ E] :
theorem starₗᵢ_apply {𝕜 : Type u_1} {E : Type u_2} [star_ring 𝕜] [ E] [ E] {x : E} :
(starₗᵢ 𝕜) x =
@[simp]
theorem starₗᵢ_to_continuous_linear_equiv {𝕜 : Type u_1} {E : Type u_2} [star_ring 𝕜] [ E] [ E] :
@[protected, instance]
def star_subalgebra.to_normed_algebra {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [star_ring 𝕜] [star_ring A] [ A] [ A] (S : A) :
Equations
@[protected, instance]
def star_subalgebra.to_cstar_ring {R : Type u_1} {A : Type u_2} [comm_ring R] [star_ring R] [normed_ring A] [star_ring A] [cstar_ring A] [ A] [ A] (S : A) :