Classes of C⋆-algebras

This file defines classes for complex C⋆-algebras. These are (unital or non-unital, commutative or noncommutative) Banach algebra over ℂ with an antimultiplicative conjugate-linear involution (star) satisfying the C⋆-identity ∥star x * x∥ = ∥x∥ ^ 2.

Notes

These classes are not defined in Mathlib/Analysis/CStarAlgebra/Basic.lean because they require heavier imports.

class NonUnitalCStarAlgebra (A : Type u_1) extends NonUnitalNormedRing A, StarRing A, CompleteSpace A, CStarRing A, NormedSpace ℂ A, IsScalarTower ℂ A A, SMulCommClass ℂ A A, StarModule ℂ A : Type u_1

The class of non-unital (complex) C⋆-algebras.

• norm : A → ℝ
• add : A → A → A
• add_assoc (a b c : A) : a + b + c = a + (b + c)
• zero : A
• zero_add (a : A) : 0 + a = a
• add_zero (a : A) : a + 0 = a
• nsmul : ℕ → A → A
• nsmul_zero (x : A) : 0 • x = 0
• nsmul_succ (n : ℕ) (x : A) : (n + 1) • x = n • x + x
• neg : A → A
• sub : A → A → A
• zsmul : ℤ → A → A
• sub_eq_add_neg (a b : A) : a - b = a + -b
• zsmul_zero' (a : A) : 0 • a = 0
• zsmul_succ' (n : ℕ) (a : A) : ↑n.succ • a = ↑n • a + a
• zsmul_neg' (n : ℕ) (a : A) : Int.negSucc n • a = -(↑n.succ • a)
• neg_add_cancel (a : A) : -a + a = 0
• add_comm (a b : A) : a + b = b + a
• mul : A → A → A
• left_distrib (a b c : A) : a * (b + c) = a * b + a * c
• right_distrib (a b c : A) : (a + b) * c = a * c + b * c
• zero_mul (a : A) : 0 * a = 0
• mul_zero (a : A) : a * 0 = 0
• mul_assoc (a b c : A) : a * b * c = a * (b * c)
• dist : A → A → ℝ
• dist_self (x : A) : dist x x = 0
• dist_comm (x y : A) : dist x y = dist y x
• dist_triangle (x y z : A) : dist x z ≤ dist x y + dist y z
• edist : A → A → ENNReal
• edist_dist (x y : A) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace A
• uniformity_dist : uniformity A = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : A × A | dist p.1 p.2 < ε}
• toBornology : Bornology A
• cobounded_sets : (Bornology.cobounded A).sets = {s : Set A | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : A} : dist x y = 0 → x = y
• dist_eq (x y : A) : dist x y = ‖-x + y‖
• norm_mul_le (a b : A) : ‖a * b‖ ≤ ‖a‖ * ‖b‖
• star : A → A
• star_involutive : Function.Involutive star
• star_mul (r s : A) : star (r * s) = star s * star r
• star_add (r s : A) : star (r + s) = star r + star s
• complete {f : Filter A} : Cauchy f → ∃ (x : A), f ≤ nhds x
• norm_mul_self_le (x : A) : ‖x‖ * ‖x‖ ≤ ‖star x * x‖
• smul : ℂ → A → A
• mul_smul (x y : ℂ) (b : A) : (x * y) • b = x • y • b
• one_smul (b : A) : 1 • b = b
• smul_zero (a : ℂ) : a • 0 = 0
• smul_add (a : ℂ) (x y : A) : a • (x + y) = a • x + a • y
• add_smul (r s : ℂ) (x : A) : (r + s) • x = r • x + s • x
• zero_smul (x : A) : 0 • x = 0
• norm_smul_le (a : ℂ) (b : A) : ‖a • b‖ ≤ ‖a‖ * ‖b‖
• smul_assoc (x : ℂ) (y z : A) : (x • y) • z = x • y • z
• smul_comm (m : ℂ) (n a : A) : m • n • a = n • m • a
• star_smul (r : ℂ) (a : A) : star (r • a) = star r • star a

class NonUnitalCommCStarAlgebra (A : Type u_1) extends NonUnitalNormedCommRing A, NonUnitalCStarAlgebra A : Type u_1

The class of non-unital commutative (complex) C⋆-algebras.

• norm : A → ℝ
• add : A → A → A
• add_assoc (a b c : A) : a + b + c = a + (b + c)
• zero : A
• zero_add (a : A) : 0 + a = a
• add_zero (a : A) : a + 0 = a
• nsmul : ℕ → A → A
• nsmul_zero (x : A) : 0 • x = 0
• nsmul_succ (n : ℕ) (x : A) : (n + 1) • x = n • x + x
• neg : A → A
• sub : A → A → A
• zsmul : ℤ → A → A
• sub_eq_add_neg (a b : A) : a - b = a + -b
• zsmul_zero' (a : A) : 0 • a = 0
• zsmul_succ' (n : ℕ) (a : A) : ↑n.succ • a = ↑n • a + a
• zsmul_neg' (n : ℕ) (a : A) : Int.negSucc n • a = -(↑n.succ • a)
• neg_add_cancel (a : A) : -a + a = 0
• add_comm (a b : A) : a + b = b + a
• mul : A → A → A
• left_distrib (a b c : A) : a * (b + c) = a * b + a * c
• right_distrib (a b c : A) : (a + b) * c = a * c + b * c
• zero_mul (a : A) : 0 * a = 0
• mul_zero (a : A) : a * 0 = 0
• mul_assoc (a b c : A) : a * b * c = a * (b * c)
• dist : A → A → ℝ
• dist_self (x : A) : dist x x = 0
• dist_comm (x y : A) : dist x y = dist y x
• dist_triangle (x y z : A) : dist x z ≤ dist x y + dist y z
• edist : A → A → ENNReal
• edist_dist (x y : A) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace A
• uniformity_dist : uniformity A = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : A × A | dist p.1 p.2 < ε}
• toBornology : Bornology A
• cobounded_sets : (Bornology.cobounded A).sets = {s : Set A | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : A} : dist x y = 0 → x = y
• dist_eq (x y : A) : dist x y = ‖-x + y‖
• norm_mul_le (a b : A) : ‖a * b‖ ≤ ‖a‖ * ‖b‖
• mul_comm (a b : A) : a * b = b * a
• star : A → A
• star_involutive : Function.Involutive star
• star_mul (r s : A) : star (r * s) = star s * star r
• star_add (r s : A) : star (r + s) = star r + star s
• complete {f : Filter A} : Cauchy f → ∃ (x : A), f ≤ nhds x
• norm_mul_self_le (x : A) : ‖x‖ * ‖x‖ ≤ ‖star x * x‖
• smul : ℂ → A → A
• mul_smul (x y : ℂ) (b : A) : (x * y) • b = x • y • b
• one_smul (b : A) : 1 • b = b
• smul_zero (a : ℂ) : a • 0 = 0
• smul_add (a : ℂ) (x y : A) : a • (x + y) = a • x + a • y
• add_smul (r s : ℂ) (x : A) : (r + s) • x = r • x + s • x
• zero_smul (x : A) : 0 • x = 0
• norm_smul_le (a : ℂ) (b : A) : ‖a • b‖ ≤ ‖a‖ * ‖b‖
• smul_assoc (x : ℂ) (y z : A) : (x • y) • z = x • y • z
• smul_comm (m : ℂ) (n a : A) : m • n • a = n • m • a
• star_smul (r : ℂ) (a : A) : star (r • a) = star r • star a

class CStarAlgebra (A : Type u_1) extends NormedRing A, StarRing A, CompleteSpace A, CStarRing A, NormedAlgebra ℂ A, StarModule ℂ A : Type u_1

The class of unital (complex) C⋆-algebras.

• norm : A → ℝ
• add : A → A → A
• add_assoc (a b c : A) : a + b + c = a + (b + c)
• zero : A
• zero_add (a : A) : 0 + a = a
• add_zero (a : A) : a + 0 = a
• nsmul : ℕ → A → A
• nsmul_zero (x : A) : 0 • x = 0
• nsmul_succ (n : ℕ) (x : A) : (n + 1) • x = n • x + x
• add_comm (a b : A) : a + b = b + a
• mul : A → A → A
• mul_assoc (a b c : A) : a * b * c = a * (b * c)
• one : A
• one_mul (a : A) : 1 * a = a
• mul_one (a : A) : a * 1 = a
• npow : ℕ → A → A
• npow_zero (x : A) : x ^ 0 = 1
• npow_succ (n : ℕ) (x : A) : x ^ (n + 1) = x ^ n * x
• zero_mul (a : A) : 0 * a = 0
• mul_zero (a : A) : a * 0 = 0
• left_distrib (a b c : A) : a * (b + c) = a * b + a * c
• right_distrib (a b c : A) : (a + b) * c = a * c + b * c
• natCast : ℕ → A
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• neg : A → A
• sub : A → A → A
• zsmul : ℤ → A → A
• sub_eq_add_neg (a b : A) : a - b = a + -b
• zsmul_zero' (a : A) : 0 • a = 0
• zsmul_succ' (n : ℕ) (a : A) : ↑n.succ • a = ↑n • a + a
• zsmul_neg' (n : ℕ) (a : A) : Int.negSucc n • a = -(↑n.succ • a)
• neg_add_cancel (a : A) : -a + a = 0
• intCast : ℤ → A
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• dist : A → A → ℝ
• dist_self (x : A) : dist x x = 0
• dist_comm (x y : A) : dist x y = dist y x
• dist_triangle (x y z : A) : dist x z ≤ dist x y + dist y z
• edist : A → A → ENNReal
• edist_dist (x y : A) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace A
• uniformity_dist : uniformity A = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : A × A | dist p.1 p.2 < ε}
• toBornology : Bornology A
• cobounded_sets : (Bornology.cobounded A).sets = {s : Set A | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : A} : dist x y = 0 → x = y
• dist_eq (x y : A) : dist x y = ‖-x + y‖
• norm_mul_le (a b : A) : ‖a * b‖ ≤ ‖a‖ * ‖b‖
• star : A → A
• star_involutive : Function.Involutive star
• star_mul (r s : A) : star (r * s) = star s * star r
• star_add (r s : A) : star (r + s) = star r + star s
• complete {f : Filter A} : Cauchy f → ∃ (x : A), f ≤ nhds x
• norm_mul_self_le (x : A) : ‖x‖ * ‖x‖ ≤ ‖star x * x‖
• smul : ℂ → A → A
• algebraMap : ℂ →+* A
• commutes' (r : ℂ) (x : A) : (algebraMap ℂ A) r * x = x * (algebraMap ℂ A) r
• smul_def' (r : ℂ) (x : A) : r • x = (algebraMap ℂ A) r * x
• norm_smul_le (r : ℂ) (x : A) : ‖r • x‖ ≤ ‖r‖ * ‖x‖
• star_smul (r : ℂ) (a : A) : star (r • a) = star r • star a

class CommCStarAlgebra (A : Type u_1) extends NormedCommRing A, CStarAlgebra A : Type u_1

The class of unital commutative (complex) C⋆-algebras.

• norm : A → ℝ
• add : A → A → A
• add_assoc (a b c : A) : a + b + c = a + (b + c)
• zero : A
• zero_add (a : A) : 0 + a = a
• add_zero (a : A) : a + 0 = a
• nsmul : ℕ → A → A
• nsmul_zero (x : A) : 0 • x = 0
• nsmul_succ (n : ℕ) (x : A) : (n + 1) • x = n • x + x
• add_comm (a b : A) : a + b = b + a
• mul : A → A → A
• mul_assoc (a b c : A) : a * b * c = a * (b * c)
• one : A
• one_mul (a : A) : 1 * a = a
• mul_one (a : A) : a * 1 = a
• npow : ℕ → A → A
• npow_zero (x : A) : x ^ 0 = 1
• npow_succ (n : ℕ) (x : A) : x ^ (n + 1) = x ^ n * x
• zero_mul (a : A) : 0 * a = 0
• mul_zero (a : A) : a * 0 = 0
• left_distrib (a b c : A) : a * (b + c) = a * b + a * c
• right_distrib (a b c : A) : (a + b) * c = a * c + b * c
• natCast : ℕ → A
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• neg : A → A
• sub : A → A → A
• zsmul : ℤ → A → A
• sub_eq_add_neg (a b : A) : a - b = a + -b
• zsmul_zero' (a : A) : 0 • a = 0
• zsmul_succ' (n : ℕ) (a : A) : ↑n.succ • a = ↑n • a + a
• zsmul_neg' (n : ℕ) (a : A) : Int.negSucc n • a = -(↑n.succ • a)
• neg_add_cancel (a : A) : -a + a = 0
• intCast : ℤ → A
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• dist : A → A → ℝ
• dist_self (x : A) : dist x x = 0
• dist_comm (x y : A) : dist x y = dist y x
• dist_triangle (x y z : A) : dist x z ≤ dist x y + dist y z
• edist : A → A → ENNReal
• edist_dist (x y : A) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace A
• uniformity_dist : uniformity A = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : A × A | dist p.1 p.2 < ε}
• toBornology : Bornology A
• cobounded_sets : (Bornology.cobounded A).sets = {s : Set A | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : A} : dist x y = 0 → x = y
• dist_eq (x y : A) : dist x y = ‖-x + y‖
• norm_mul_le (a b : A) : ‖a * b‖ ≤ ‖a‖ * ‖b‖
• mul_comm (a b : A) : a * b = b * a
• star : A → A
• star_involutive : Function.Involutive star
• star_mul (r s : A) : star (r * s) = star s * star r
• star_add (r s : A) : star (r + s) = star r + star s
• complete {f : Filter A} : Cauchy f → ∃ (x : A), f ≤ nhds x
• norm_mul_self_le (x : A) : ‖x‖ * ‖x‖ ≤ ‖star x * x‖
• smul : ℂ → A → A
• algebraMap : ℂ →+* A
• commutes' (r : ℂ) (x : A) : (algebraMap ℂ A) r * x = x * (algebraMap ℂ A) r
• smul_def' (r : ℂ) (x : A) : r • x = (algebraMap ℂ A) r * x
• norm_smul_le (r : ℂ) (x : A) : ‖r • x‖ ≤ ‖r‖ * ‖x‖
• star_smul (r : ℂ) (a : A) : star (r • a) = star r • star a

@[instance_reducible, instance 100]

noncomputable instance CStarAlgebra.toNonUnitalCStarAlgebra (A : Type u_1) [CStarAlgebra A] : NonUnitalCStarAlgebra A

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible, instance 100]

noncomputable instance CommCStarAlgebra.toNonUnitalCommCStarAlgebra (A : Type u_1) [CommCStarAlgebra A] : NonUnitalCommCStarAlgebra A

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance StarSubalgebra.cstarAlgebra {S : Type u_1} {A : Type u_2} [CStarAlgebra A] [SetLike S A] [SubringClass S A] [SMulMemClass S ℂ A] [StarMemClass S A] (s : S) [h_closed : IsClosed ↑s] : CStarAlgebra ↥s

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance StarSubalgebra.commCStarAlgebra {S : Type u_1} {A : Type u_2} [CommCStarAlgebra A] [SetLike S A] [SubringClass S A] [SMulMemClass S ℂ A] [StarMemClass S A] (s : S) [h_closed : IsClosed ↑s] : CommCStarAlgebra ↥s

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance NonUnitalStarSubalgebra.nonUnitalCStarAlgebra {S : Type u_1} {A : Type u_2} [NonUnitalCStarAlgebra A] [SetLike S A] [NonUnitalSubringClass S A] [SMulMemClass S ℂ A] [StarMemClass S A] (s : S) [h_closed : IsClosed ↑s] : NonUnitalCStarAlgebra ↥s

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance NonUnitalStarSubalgebra.nonUnitalCommCStarAlgebra {S : Type u_1} {A : Type u_2} [NonUnitalCommCStarAlgebra A] [SetLike S A] [NonUnitalSubringClass S A] [SMulMemClass S ℂ A] [StarMemClass S A] (s : S) [h_closed : IsClosed ↑s] : NonUnitalCommCStarAlgebra ↥s

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance instCommCStarAlgebraComplex : CommCStarAlgebra ℂ

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

def IsMulCommutative.instNonUnitalCommCStarAlgebra {A : Type u_1} [NonUnitalCStarAlgebra A] [IsMulCommutative A] : NonUnitalCommCStarAlgebra A

A NonUnitalCStarAlgebra which IsMulCommutative is a NonUnitalCommCStarAlgebra.

This is primarily used to deduce the bundled version from the unbundled one for commutative subobjects in a noncommutative ambient type. As such this is only available inside the IsMulCommutative scope so as to avoid deleterious effects to type class synthesis for bundled commutativity.

See note [commutative subobjects].

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

def IsMulCommutative.instCommCStarAlgebra {A : Type u_1} [CStarAlgebra A] [IsMulCommutative A] : CommCStarAlgebra A

A CStarAlgebra which IsMulCommutative is a CommCStarAlgebra.

This is primarily used to deduce the bundled version from the unbundled one for commutative subobjects in a noncommutative ambient type. As such this is only available inside the IsMulCommutative scope so as to avoid deleterious effects to type class synthesis for bundled commutativity.

See note [commutative subobjects].

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance instCStarAlgebraSubtypeMemStarSubalgebraComplexElemental {A : Type u_1} [CStarAlgebra A] (x : A) : CStarAlgebra ↥(StarAlgebra.elemental ℂ x)

Equations

• instCStarAlgebraSubtypeMemStarSubalgebraComplexElemental x = StarSubalgebra.cstarAlgebra (StarAlgebra.elemental ℂ x)

@[instance_reducible]

noncomputable instance instNonUnitalCStarAlgebraSubtypeMemNonUnitalStarSubalgebraComplexElemental {A : Type u_1} [NonUnitalCStarAlgebra A] (x : A) : NonUnitalCStarAlgebra ↥(NonUnitalStarAlgebra.elemental ℂ x)

Equations

• instNonUnitalCStarAlgebraSubtypeMemNonUnitalStarSubalgebraComplexElemental x = NonUnitalStarSubalgebra.nonUnitalCStarAlgebra (NonUnitalStarAlgebra.elemental ℂ x)

@[instance_reducible]

noncomputable instance instCommCStarAlgebraSubtypeMemStarSubalgebraComplexElementalOfIsStarNormal {A : Type u_1} [CStarAlgebra A] (x : A) [IsStarNormal x] : CommCStarAlgebra ↥(StarAlgebra.elemental ℂ x)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance instNonUnitalCommCStarAlgebraSubtypeMemNonUnitalStarSubalgebraComplexElementalOfIsStarNormal {A : Type u_1} [NonUnitalCStarAlgebra A] (x : A) [IsStarNormal x] : NonUnitalCommCStarAlgebra ↥(NonUnitalStarAlgebra.elemental ℂ x)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance instNonUnitalCStarAlgebraForall {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [(i : ι) → NonUnitalCStarAlgebra (A i)] : NonUnitalCStarAlgebra ((i : ι) → A i)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance instNonUnitalCommCStarAlgebraForall {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [(i : ι) → NonUnitalCommCStarAlgebra (A i)] : NonUnitalCommCStarAlgebra ((i : ι) → A i)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance instCStarAlgebraForall {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [(i : ι) → CStarAlgebra (A i)] : CStarAlgebra ((i : ι) → A i)

Equations

• instCStarAlgebraForall = { toNormedRing := Pi.normedRing, toStarRing := Pi.starRing', toCompleteSpace := ⋯, toCStarRing := ⋯, toNormedAlgebra := Pi.normedAlgebra ℂ, toStarModule := ⋯ }

@[instance_reducible]

noncomputable instance instCommCStarAlgebraForall {ι : Type u_1} {A : ι → Type u_2} [Fintype ι] [(i : ι) → CommCStarAlgebra (A i)] : CommCStarAlgebra ((i : ι) → A i)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance instNonUnitalCStarAlgebraProd {A : Type u_1} {B : Type u_2} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] : NonUnitalCStarAlgebra (A × B)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance instNonUnitalCommCStarAlgebraProd {A : Type u_1} {B : Type u_2} [NonUnitalCommCStarAlgebra A] [NonUnitalCommCStarAlgebra B] : NonUnitalCommCStarAlgebra (A × B)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance instCStarAlgebraProd {A : Type u_1} {B : Type u_2} [CStarAlgebra A] [CStarAlgebra B] : CStarAlgebra (A × B)

Equations

• instCStarAlgebraProd = { toNormedRing := Prod.normedRing, toStarRing := Prod.instStarRing, toCompleteSpace := ⋯, toCStarRing := ⋯, toNormedAlgebra := Prod.normedAlgebra ℂ, toStarModule := ⋯ }

@[instance_reducible]

noncomputable instance instCommCStarAlgebraProd {A : Type u_1} {B : Type u_2} [CommCStarAlgebra A] [CommCStarAlgebra B] : CommCStarAlgebra (A × B)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance MulOpposite.instNonUnitalCStarAlgebra {A : Type u_1} [NonUnitalCStarAlgebra A] : NonUnitalCStarAlgebra Aᵐᵒᵖ

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance MulOpposite.instNonUnitalCommCStarAlgebra {A : Type u_1} [NonUnitalCommCStarAlgebra A] : NonUnitalCommCStarAlgebra Aᵐᵒᵖ

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance MulOpposite.instCStarAlgebra {A : Type u_1} [CStarAlgebra A] : CStarAlgebra Aᵐᵒᵖ

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance MulOpposite.instCommCStarAlgebra {A : Type u_1} [CommCStarAlgebra A] : CommCStarAlgebra Aᵐᵒᵖ

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev IsUnital.toCStarAlgebra {A : Type u_1} [NonUnitalCStarAlgebra A] [IsUnital A] : CStarAlgebra A

A unital non-unital C⋆-algebra is a C⋆-algebra.

This constructor is primarily intended to be used within proofs since it creates bad definitional equalities.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev IsUnital.toCommCStarAlgebra {A : Type u_1} [NonUnitalCommCStarAlgebra A] [IsUnital A] : CommCStarAlgebra A

A unital non-unital commutative C⋆-algebra is a commutative C⋆-algebra.

This constructor is primarily intended to be used within proofs since it creates bad definitional equalities.

Equations

• One or more equations did not get rendered due to their size.