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 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), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : A), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• neg : A → A
• sub : A → A → A
• sub_eq_add_neg : ∀ (a b : A), a - b = a + -b
• zsmul : ℤ → A → A
• zsmul_zero' : ∀ (a : A), SubNegMonoid.zsmul 0 a = 0
• zsmul_succ' : ∀ (n : ℕ) (a : A), SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : A), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑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), PseudoMetricSpace.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 : ∀ (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
• one_smul : ∀ (b : A), 1 • b = b
• mul_smul : ∀ (x y : ℂ) (b : A), (x * y) • b = x • y • 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), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : A), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• neg : A → A
• sub : A → A → A
• sub_eq_add_neg : ∀ (a b : A), a - b = a + -b
• zsmul : ℤ → A → A
• zsmul_zero' : ∀ (a : A), SubNegMonoid.zsmul 0 a = 0
• zsmul_succ' : ∀ (n : ℕ) (a : A), SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : A), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑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), PseudoMetricSpace.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 : ∀ (a b : A), ‖a * b‖ ≤ ‖a‖ * ‖b‖
• mul_comm : ∀ (x y : A), x * y = y * x
• 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
• one_smul : ∀ (b : A), 1 • b = b
• mul_smul : ∀ (x y : ℂ) (b : A), (x * y) • b = x • y • 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), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : A), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• 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)
• one : A
• one_mul : ∀ (a : A), 1 * a = a
• mul_one : ∀ (a : A), a * 1 = a
• natCast : ℕ → A
• natCast_zero : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → A → A
• npow_zero : ∀ (x : A), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : A), Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : A → A
• sub : A → A → A
• sub_eq_add_neg : ∀ (a b : A), a - b = a + -b
• zsmul : ℤ → A → A
• zsmul_zero' : ∀ (a : A), Ring.zsmul 0 a = 0
• zsmul_succ' : ∀ (n : ℕ) (a : A), Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : A), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑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), PseudoMetricSpace.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 : ∀ (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
• toFun : ℂ → A
• map_one' : (↑↑Algebra.toRingHom).toFun 1 = 1
• map_mul' : ∀ (x y : ℂ), (↑↑Algebra.toRingHom).toFun (x * y) = (↑↑Algebra.toRingHom).toFun x * (↑↑Algebra.toRingHom).toFun y
• map_zero' : (↑↑Algebra.toRingHom).toFun 0 = 0
• map_add' : ∀ (x y : ℂ), (↑↑Algebra.toRingHom).toFun (x + y) = (↑↑Algebra.toRingHom).toFun x + (↑↑Algebra.toRingHom).toFun y
• commutes' : ∀ (r : ℂ) (x : A), Algebra.toRingHom r * x = x * Algebra.toRingHom r
• smul_def' : ∀ (r : ℂ) (x : A), r • x = Algebra.toRingHom 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), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : A), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• 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)
• one : A
• one_mul : ∀ (a : A), 1 * a = a
• mul_one : ∀ (a : A), a * 1 = a
• natCast : ℕ → A
• natCast_zero : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → A → A
• npow_zero : ∀ (x : A), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : A), Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : A → A
• sub : A → A → A
• sub_eq_add_neg : ∀ (a b : A), a - b = a + -b
• zsmul : ℤ → A → A
• zsmul_zero' : ∀ (a : A), Ring.zsmul 0 a = 0
• zsmul_succ' : ∀ (n : ℕ) (a : A), Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : A), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑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), PseudoMetricSpace.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 : ∀ (a b : A), ‖a * b‖ ≤ ‖a‖ * ‖b‖
• mul_comm : ∀ (x y : A), x * y = y * x
• 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
• toFun : ℂ → A
• map_one' : (↑↑Algebra.toRingHom).toFun 1 = 1
• map_mul' : ∀ (x y : ℂ), (↑↑Algebra.toRingHom).toFun (x * y) = (↑↑Algebra.toRingHom).toFun x * (↑↑Algebra.toRingHom).toFun y
• map_zero' : (↑↑Algebra.toRingHom).toFun 0 = 0
• map_add' : ∀ (x y : ℂ), (↑↑Algebra.toRingHom).toFun (x + y) = (↑↑Algebra.toRingHom).toFun x + (↑↑Algebra.toRingHom).toFun y
• commutes' : ∀ (r : ℂ) (x : A), Algebra.toRingHom r * x = x * Algebra.toRingHom r
• smul_def' : ∀ (r : ℂ) (x : A), r • x = Algebra.toRingHom 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 100]

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

Equations

• CStarAlgebra.toNonUnitalCStarAlgebra A = NonUnitalCStarAlgebra.mk

@[instance 100]

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

Equations

• CommCStarAlgebra.toNonUnitalCommCStarAlgebra A = NonUnitalCommCStarAlgebra.mk

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

• StarSubalgebra.cstarAlgebra s = CStarAlgebra.mk

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

• StarSubalgebra.commCStarAlgebra s = CommCStarAlgebra.mk

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

• NonUnitalStarSubalgebra.nonUnitalCStarAlgebra s = NonUnitalCStarAlgebra.mk

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

• NonUnitalStarSubalgebra.nonUnitalCommCStarAlgebra s = NonUnitalCommCStarAlgebra.mk

noncomputable instance instCommCStarAlgebraComplex : CommCStarAlgebra ℂ

Equations

• instCommCStarAlgebraComplex = CommCStarAlgebra.mk

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

Equations

• instNonUnitalCStarAlgebraForall = NonUnitalCStarAlgebra.mk

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

Equations

• instNonUnitalCommCStarAlgebraForall = NonUnitalCommCStarAlgebra.mk

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

Equations

• instCStarAlgebraForall = CStarAlgebra.mk

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

Equations

• instCommCStarAlgebraForall = CommCStarAlgebra.mk

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

Equations

• instNonUnitalCStarAlgebraProd = NonUnitalCStarAlgebra.mk

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

Equations

• instNonUnitalCommCStarAlgebraProd = NonUnitalCommCStarAlgebra.mk

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

Equations

• instCStarAlgebraProd = CStarAlgebra.mk

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

Equations

• instCommCStarAlgebraProd = CommCStarAlgebra.mk