# Documentation

Mathlib.Analysis.NormedSpace.Star.Basic

# Normed star rings and algebras #

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 [NormedField 𝕜] [StarRing 𝕜] [NormedRing E] [StarRing E] [CstarRing E] [NormedAlgebra 𝕜 E] [StarModule 𝕜 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 NormedStarGroup (E : Type u_1) [] :

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

Instances
@[simp]
theorem nnnorm_star {E : Type u_2} [] [] (x : E) :
def starNormedAddGroupHom {E : Type u_2} [] [] :

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

Instances For
theorem star_isometry {E : Type u_2} [] [] :

The star map in a normed star group is an isometry

instance RingHomIsometric.starRingEnd {E : Type u_2} [] [] [] :
class CstarRing (E : Type u_4) [] :

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

Instances
instance CstarRing.to_normedStarGroup {E : Type u_2} [] [] :

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

theorem CstarRing.norm_self_mul_star {E : Type u_2} [] [] {x : E} :
theorem CstarRing.norm_star_mul_self' {E : Type u_2} [] [] {x : E} :
@[simp]
theorem CstarRing.star_mul_self_eq_zero_iff {E : Type u_2} [] [] (x : E) :
star x * x = 0 x = 0
theorem CstarRing.star_mul_self_ne_zero_iff {E : Type u_2} [] [] (x : E) :
star x * x 0 x 0
@[simp]
theorem CstarRing.mul_star_self_eq_zero_iff {E : Type u_2} [] [] (x : E) :
x * star x = 0 x = 0
theorem CstarRing.mul_star_self_ne_zero_iff {E : Type u_2} [] [] (x : E) :
x * star x 0 x 0
instance Pi.starRing' {ι : Type u_4} {R : ιType u_7} [(i : ι) → NonUnitalNormedRing (R i)] [(i : ι) → StarRing (R i)] :
StarRing ((i : ι) → R i)

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

instance Prod.cstarRing {R₁ : Type u_5} {R₂ : Type u_6} [] [StarRing R₁] [] [] [StarRing R₂] [] :
CstarRing (R₁ × R₂)
instance Pi.cstarRing {ι : Type u_4} {R : ιType u_7} [(i : ι) → NonUnitalNormedRing (R i)] [(i : ι) → StarRing (R i)] [] [∀ (i : ι), CstarRing (R i)] :
CstarRing ((i : ι) → R i)
instance Pi.cstarRing' {ι : Type u_4} {R₁ : Type u_5} [] [StarRing R₁] [] [] :
CstarRing (ιR₁)
@[simp]
theorem CstarRing.norm_one {E : Type u_2} [] [] [] [] :
theorem CstarRing.norm_coe_unitary {E : Type u_2} [] [] [] [] (U : { x // x }) :
U = 1
@[simp]
theorem CstarRing.norm_of_mem_unitary {E : Type u_2} [] [] [] [] {U : E} (hU : U ) :
@[simp]
theorem CstarRing.norm_coe_unitary_mul {E : Type u_2} [] [] [] (U : { x // x }) (A : E) :
U * A = A
@[simp]
theorem CstarRing.norm_unitary_smul {E : Type u_2} [] [] [] (U : { x // x }) (A : E) :
theorem CstarRing.norm_mem_unitary_mul {E : Type u_2} [] [] [] {U : E} (A : E) (hU : U ) :
@[simp]
theorem CstarRing.norm_mul_coe_unitary {E : Type u_2} [] [] [] (A : E) (U : { x // x }) :
A * U = A
theorem CstarRing.norm_mul_mem_unitary {E : Type u_2} [] [] [] (A : E) {U : E} (hU : U ) :
theorem IsSelfAdjoint.nnnorm_pow_two_pow {E : Type u_2} [] [] [] {x : E} (hx : ) (n : ) :
x ^ 2 ^ n‖₊ = x‖₊ ^ 2 ^ n
theorem selfAdjoint.nnnorm_pow_two_pow {E : Type u_2} [] [] [] (x : { x // x }) (n : ) :
x ^ 2 ^ n‖₊ = x‖₊ ^ 2 ^ n
def starₗᵢ (𝕜 : Type u_1) {E : Type u_2} [] [] [] [] [Module 𝕜 E] [] :

star bundled as a linear isometric equivalence

Instances For
@[simp]
theorem coe_starₗᵢ {𝕜 : Type u_1} {E : Type u_2} [] [] [] [] [Module 𝕜 E] [] :
↑() = star
theorem starₗᵢ_apply {𝕜 : Type u_1} {E : Type u_2} [] [] [] [] [Module 𝕜 E] [] {x : E} :
↑() x = star x
@[simp]
theorem starₗᵢ_toContinuousLinearEquiv {𝕜 : Type u_1} {E : Type u_2} [] [] [] [] [Module 𝕜 E] [] :
instance StarSubalgebra.toNormedAlgebra {𝕜 : Type u_4} {A : Type u_5} [] [] [] [] [] [] (S : ) :
NormedAlgebra 𝕜 { x // x S }
instance StarSubalgebra.to_cstarRing {R : Type u_4} {A : Type u_5} [] [] [] [] [] [Algebra R A] [] (S : ) :
CstarRing { x // x S }