feat: IsUnital class

LeanOA.lean

@@ -6,6 +6,7 @@ import LeanOA.CStarAlgebra.PositiveLinearFunctional
 import LeanOA.CStarModule.Standard
 import LeanOA.ComplexOrder
 import LeanOA.ExtremallyDisconnected
+import LeanOA.IsUnital
 import LeanOA.KreinSmulian
 import LeanOA.Lp.Holder
 import LeanOA.Lp.lpSpace
@@ -17,7 +18,6 @@ import LeanOA.Mathlib.Algebra.Order.Star.Conjugate
 import LeanOA.Mathlib.Algebra.Star.StarAlgHom
 import LeanOA.Mathlib.Algebra.Star.Unitary
 import LeanOA.Mathlib.Analysis.CStarAlgebra.ApproximateUnit
-import LeanOA.Mathlib.Analysis.CStarAlgebra.Basic
 import LeanOA.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
 import LeanOA.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
 import LeanOA.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Transfer

LeanOA/CStarAlgebra/Extreme.lean

@@ -1,27 +1,29 @@
 import LeanOA.CFC
+import LeanOA.IsUnital
 import LeanOA.Mathlib.Analysis.CStarAlgebra.ApproximateUnit
-import LeanOA.Mathlib.Analysis.CStarAlgebra.Basic
 import LeanOA.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
 import LeanOA.Mathlib.Analysis.CStarAlgebra.GelfandDuality
 import Mathlib.Analysis.Convex.Extreme
+import Mathlib.Analysis.Convex.Strict.Extreme
+import Mathlib.Analysis.CStarAlgebra.Unitary.Maps
 import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
 
 /-! # Extreme points of the closed unit ball in C⋆-algebras
 
 This file contains results on the extreme points of the closed unit ball in (unital) C⋆-algebras.
 In particular, we show that in a C⋆-algebra :
 
-* `CStarAlgebra.one_mem_extremePoints_closedUnitBall`, `CStarAlgebra.ofExtremePt`:
+* `CStarAlgebra.isUnital_iff`:
   A C⋆-algebra is unital if and only if there exists an extreme point of the closed unit ball.
-* `isStarProjection_iff_mem_extremePoints_nonneg_and_mem_closedUnitBall`:
+* `isStarProjection_iff_mem_extremePoints_nonneg_and_mem_unitClosedBall`:
   The extreme points of the nonnegative closed unit ball are its projections.
-* `mem_extremePoints_isSelfAdjoint_and_mem_closedUnitBall_iff_isSelfAdjoint_and_mem_unitary`:
+* `mem_extremePoints_isSelfAdjoint_and_mem_unitClosedBall_iff_isSelfAdjoint_and_mem_unitary`:
   The extreme points of the self-adjoint closed unit ball are its self-adjoint unitaries.
 
 ## TODO
 
 * Generalize
-  `mem_extremePoints_isSelfAdjoint_and_mem_closedUnitBall_iff_isSelfAdjoint_and_mem_unitary` to
+  `mem_extremePoints_isSelfAdjoint_and_mem_unitClosedBall_iff_isSelfAdjoint_and_mem_unitary` to
   non-unital by showing that the existence of an extreme point in the closed unit ball of the
   self-adjoint elements implies the algebra is unital.)
   Here is an outline from Jireh that will work:
@@ -42,24 +44,8 @@ In particular, we show that in a C⋆-algebra :
 
 open Set Metric CFC CStarAlgebra Unitization
 
--- move to...?
-@[simp]
-lemma Set.extremePoints_Icc {a b : ℝ} (hab : a ≤ b) :
-    Set.extremePoints ℝ (Icc a b) = {a, b} := by
-  ext x
-  rw [convex_Icc .. |>.mem_extremePoints_iff_convex_diff]
-  constructor
-  · intro ⟨h₁, h₂⟩
-    suffices x ∉ Ioo a b by grind
-    intro hx
-    have := h₂.isPreconnected.Icc_subset (a := a) (b := b) (by grind) (by grind)
-    grind
-  · rintro (rfl | rfl)
-    · simpa using ⟨hab, convex_Ioc ..⟩
-    · simpa using ⟨hab, convex_Ico ..⟩
-
 open scoped ComplexStarModule in
-lemma CStarAlgebra.one_mem_extremePoints_closedUnitBall {A : Type*} [CStarAlgebra A] :
+lemma CStarAlgebra.one_mem_extremePoints_unitClosedBall {A : Type*} [CStarAlgebra A] :
     1 ∈ extremePoints ℝ (closedBall (0 : A) 1) := by
   nontriviality A
   /- Suppose that `1` is a convex combination of `x` and `y`. Then, since `1` is self
@@ -117,16 +103,15 @@ lemma CStarAlgebra.one_mem_extremePoints_closedUnitBall {A : Type*} [CStarAlgebr
   rw [← norm_eq_zero, ← sq_eq_zero_iff, ← IsSelfAdjoint.norm_mul_self (ℑ x).2, ← sq, norm_eq_zero]
   exact le_antisymm (by simpa using hx) (ℑ x).2.sq_nonneg
 
-lemma Unitary.coe_mem_extremePoints_closedUnitBall {A : Type*} [CStarAlgebra A] (u : unitary A) :
+lemma Unitary.coe_mem_extremePoints_unitClosedBall {A : Type*} [CStarAlgebra A] (u : unitary A) :
     (u : A) ∈ extremePoints ℝ (closedBall 0 1) := by
-  rw [← map_zero (mulLeftLinearIsometryEquiv ℝ A u), ← LinearIsometryEquiv.image_closedBall,
-    ← image_extremePoints]
-  exact ⟨1 , ⟨one_mem_extremePoints_closedUnitBall, by simp⟩⟩
+  rw [← map_zero (mulLeft ℝ A u), ← LinearIsometryEquiv.image_closedBall, ← image_extremePoints]
+  exact ⟨1 , ⟨one_mem_extremePoints_unitClosedBall, by simp⟩⟩
 
 section nonUnital
 variable {A : Type*} [NonUnitalCStarAlgebra A]
 
-theorem star_self_conjugate_eq_self_of_mem_extremePoints_closedUnitBall {a : A}
+theorem star_self_conjugate_eq_self_of_mem_extremePoints_unitClosedBall {a : A}
     (ha : a ∈ extremePoints ℝ (closedBall 0 1)) : a * star a * a = a := by
   /- Suppose `a` is an extreme point of the closed unit ball. Then we want to show that
   `a * star a * a = a`. It suffices to show `a * |a| = a`. -/
@@ -161,15 +146,15 @@ attribute [local grind] IsStarProjection
 
 /-- Every extreme point in the closed unit ball of a `NonUnitalCStarAlgebra` is a
 partial isometry (in other words, `star a * a` is a projection). -/
-theorem isStarProjection_star_mul_self_of_mem_extremePoints_closedUnitBall
+theorem isStarProjection_star_mul_self_of_mem_extremePoints_unitClosedBall
     {a : A} (ha : a ∈ extremePoints ℝ (closedBall 0 1)) : IsStarProjection (star a * a) := by
-  grind [star_self_conjugate_eq_self_of_mem_extremePoints_closedUnitBall ha]
+  grind [star_self_conjugate_eq_self_of_mem_extremePoints_unitClosedBall ha]
 
 /-- Every extreme point in the closed unit ball of a `NonUnitalCStarAlgebra` is a
 partial isometry (in other words, `a * star a` is a projection). -/
-theorem isStarProjection_self_mul_star_of_mem_extremePoints_closedUnitBall
+theorem isStarProjection_self_mul_star_of_mem_extremePoints_unitClosedBall
     {a : A} (ha : a ∈ extremePoints ℝ (closedBall 0 1)) : IsStarProjection (a * star a) := by
-  grind [star_self_conjugate_eq_self_of_mem_extremePoints_closedUnitBall ha]
+  grind [star_self_conjugate_eq_self_of_mem_extremePoints_unitClosedBall ha]
 
 variable {A : Type*} [NonUnitalCStarAlgebra A]
 
@@ -180,12 +165,12 @@ shorthand used in paper proofs to make them more transparent, but it is
 nonsense to refer to `1`, and the notation means that everything should be
 considered as fully expanded. This is reflected in the statement below.
 *The converse is Sakai 1.6.4.* -/
-private theorem eq_zero_of_eq_sub_of_mem_closedBall_of_mem_extremePoints_closedUnitBall
+private theorem eq_zero_of_eq_sub_of_mem_closedBall_of_mem_extremePoints_unitClosedBall
     {x a b : A} (hx : x ∈ extremePoints ℝ (closedBall 0 1)) (ha : a ∈ closedBall 0 1)
     (hb : a = b - b * (star x * x) - (x * star x) * b + (x * star x) * b * (star x * x)) :
     a = 0 := by
-  have hP := isStarProjection_star_mul_self_of_mem_extremePoints_closedUnitBall hx
-  have hQ := isStarProjection_self_mul_star_of_mem_extremePoints_closedUnitBall hx
+  have hP := isStarProjection_star_mul_self_of_mem_extremePoints_unitClosedBall hx
+  have hQ := isStarProjection_self_mul_star_of_mem_extremePoints_unitClosedBall hx
   set p := star x * x with hp
   /- Notice that `x = q * x * p`, and `star x = p * star x * q` formally yield
   `star x * (1 - q) * b * (1 - p) = 0` with the above abusive notation. By substituting for `a` in
@@ -230,7 +215,7 @@ theorem CStarAlgebra.mul_ofExtremePtOne {x : A} (hx : x ∈ extremePoints ℝ (c
   let hu := increasingApproximateUnit A
   let f (t : A) : A := t - t * (star x * x) - x * star x * t + x * star x * t * (star x * x)
   have h (t : A) : f t = 0 := by
-    simpa using eq_zero_of_eq_sub_of_mem_closedBall_of_mem_extremePoints_closedUnitBall
+    simpa using eq_zero_of_eq_sub_of_mem_closedBall_of_mem_extremePoints_unitClosedBall
       hx (inv_norm_smul_mem_unitClosedBall (f t)) (b := ‖f t‖⁻¹ • t)
       (by simp [← mul_assoc, smul_mul_assoc, mul_smul_comm, sub_sub, ← smul_sub, ← smul_add, f])
   have h_tendsto : Tendsto (fun t ↦ a * f t) u
@@ -258,30 +243,18 @@ theorem CStarAlgebra.ofExtremePtOne_mul {x : A} (hx : x ∈ extremePoints ℝ (c
     (a : A) : (star x * x + x * star x - x * star x * (star x * x)) * a = a := by
   simpa [add_comm] using congr(star $(mul_ofExtremePtOne (x := star x) (by simpa) (star a)))
 
-/-- The ring structure given an extreme point of the closed unit ball on a non-unital
-C⋆-algebra. Only an implementation for `CStarAlgebra.ofExtremePt`. -/
-abbrev CStarAlgebra.ringOfExtremePt {x : A} (hx : x ∈ extremePoints ℝ (closedBall 0 1)) :
-    Ring A where
-  one := star x * x + x * star x - x * star x * (star x * x)
-  one_mul y := ofExtremePtOne_mul hx y
-  mul_one y := mul_ofExtremePtOne hx y
-
-lemma CStarAlgebra.ofExtremePt_one_def {x : A} (hx : x ∈ extremePoints ℝ (closedBall 0 1)) :
-    letI := CStarAlgebra.ringOfExtremePt hx
-    1 = star x * x + x * star x - x * star x * (star x * x) :=
-  rfl
+attribute [local instance] IsUnital.toCStarAlgebra in
+/-- A C⋆-algebra is unital iff there exists an extreme point of the closed unit ball.
 
-/-- Upgrade a non-unital C⋆-algebra to a unital C⋆-algebra, given there exists an
-extreme point of the closed unit ball. -/
-abbrev CStarAlgebra.ofExtremePt {x : A} (hx : x ∈ extremePoints ℝ (closedBall 0 1)) :
-    CStarAlgebra A where
-  __ := ‹NonUnitalCStarAlgebra A›
-  __ := ringOfExtremePt hx
-  __ := Algebra.ofModule smul_mul_assoc mul_smul_comm
+To upgrade a non-unital C⋆-algebra to a unital one, use `IsUnital.toCStarAlgebra`. -/
+theorem CStarAlgebra.isUnital_iff :
+    IsUnital A ↔ ∃ x : A, x ∈ extremePoints ℝ (closedBall (0 : A) 1) := by
+  refine ⟨fun h ↦ ⟨1, one_mem_extremePoints_unitClosedBall⟩, fun ⟨x, hx⟩ ↦ ?_⟩
+  exact ⟨_, fun y ↦ ⟨ofExtremePtOne_mul hx y, mul_ofExtremePtOne hx y⟩⟩
 
 /-- The star projections in a non-unital C⋆-algebra are exactly the extreme points of
 the nonnegative closed unit ball. -/
-theorem isStarProjection_iff_mem_extremePoints_nonneg_and_mem_closedUnitBall
+theorem isStarProjection_iff_mem_extremePoints_nonneg_and_mem_unitClosedBall
     [PartialOrder A] [StarOrderedRing A] {e : A} :
     IsStarProjection e ↔ e ∈ extremePoints ℝ {x : A | 0 ≤ x ∧ x ∈ closedBall 0 1} := by
   simp only [mem_closedBall, dist_zero_right, mem_extremePoints_iff_left, mem_setOf_eq, and_imp]
@@ -336,12 +309,12 @@ private lemma CStarAlgebra.norm_sub_le_one_of_nonneg_of_norm_le_one [PartialOrde
     (by simpa using add_le_add hx.inr (neg_le_neg_iff.mpr hy0))
     (add_le_add hx0 (by simpa using neg_le_neg hy.inr : -(y : A⁺¹) ≤ 0))
 
-theorem isStarProjection_posPart_of_mem_extremePoints_isSelfAdjoint_and_mem_closedUnitBall
+theorem isStarProjection_posPart_of_mem_extremePoints_isSelfAdjoint_and_mem_unitClosedBall
     {e : A} (he : e ∈ extremePoints ℝ {x | IsSelfAdjoint x ∧ x ∈ closedBall 0 1}) :
     IsStarProjection (e⁺ : A) := by
   let := spectralOrder A
   let := spectralOrderedRing A
-  rw [isStarProjection_iff_mem_extremePoints_nonneg_and_mem_closedUnitBall]
+  rw [isStarProjection_iff_mem_extremePoints_nonneg_and_mem_unitClosedBall]
   simp only [mem_closedBall_zero_iff, mem_extremePoints_iff_left, mem_setOf_eq] at he ⊢
   refine ⟨⟨posPart_nonneg e, ?_⟩, fun x hx y hy ⟨α, β, hα, hβ, hαβ, h⟩ ↦ ?_⟩
   · grw [norm_posPart_le, he.1.2]
@@ -353,12 +326,12 @@ theorem isStarProjection_posPart_of_mem_extremePoints_isSelfAdjoint_and_mem_clos
   refine hpn ▸ sub_eq_iff_eq_add.mp <| this ⟨α, β, hα, hβ, hαβ, ?_⟩
   simp [smul_sub, sub_add_sub_comm, ← add_smul, hαβ, sub_eq_iff_eq_add, ← hpn, h]
 
-theorem isStarProjection_negPart_of_mem_extremePoints_isSelfAdjoint_and_mem_closedUnitBall
+theorem isStarProjection_negPart_of_mem_extremePoints_isSelfAdjoint_and_mem_unitClosedBall
     {e : A} (he : e ∈ Set.extremePoints ℝ {x | IsSelfAdjoint x ∧ x ∈ closedBall 0 1}) :
     IsStarProjection (e⁻ : A) := by
   let := spectralOrder A
   let := spectralOrderedRing A
-  rw [isStarProjection_iff_mem_extremePoints_nonneg_and_mem_closedUnitBall]
+  rw [isStarProjection_iff_mem_extremePoints_nonneg_and_mem_unitClosedBall]
   simp only [mem_closedBall_zero_iff, mem_extremePoints_iff_left, mem_setOf_eq] at he ⊢
   refine ⟨⟨negPart_nonneg e, ?_⟩, fun x hx y hy ⟨α, β, hα, hβ, hαβ, h⟩ ↦ ?_⟩
   · grw [norm_negPart_le, he.1.2]
@@ -376,13 +349,13 @@ end nonUnital
 
 /-- The extreme points of the self-adjoint closed unit ball is exactly the set of self-adjoint
 unitaries. -/
-theorem mem_extremePoints_isSelfAdjoint_and_mem_closedUnitBall_iff_isSelfAdjoint_and_mem_unitary
+theorem mem_extremePoints_isSelfAdjoint_and_mem_unitClosedBall_iff_isSelfAdjoint_and_mem_unitary
     {A : Type*} [CStarAlgebra A] {e : A} :
     e ∈ extremePoints ℝ {x | IsSelfAdjoint x ∧ x ∈ closedBall 0 1} ↔
       IsSelfAdjoint e ∧ e ∈ unitary A := by
   refine ⟨fun he ↦ ⟨(mem_setOf_eq ▸ he.1).1, ?_⟩, fun he ↦ ?_⟩
-  · have h1 := isStarProjection_negPart_of_mem_extremePoints_isSelfAdjoint_and_mem_closedUnitBall he
-    have h2 := isStarProjection_posPart_of_mem_extremePoints_isSelfAdjoint_and_mem_closedUnitBall he
+  · have h1 := isStarProjection_negPart_of_mem_extremePoints_isSelfAdjoint_and_mem_unitClosedBall he
+    have h2 := isStarProjection_posPart_of_mem_extremePoints_isSelfAdjoint_and_mem_unitClosedBall he
     simp only [mem_closedBall_zero_iff, mem_extremePoints_iff_left, mem_setOf_eq] at he
     rw [Unitary.mem_iff, he.1.1, and_self, ← posPart_sub_negPart e he.1.1]
     simp only [mul_sub, sub_mul, h2.isIdempotentElem.eq, negPart_mul_posPart, sub_zero,
@@ -398,16 +371,16 @@ theorem mem_extremePoints_isSelfAdjoint_and_mem_closedUnitBall_iff_isSelfAdjoint
     · grw [he.1.1.norm_sub_eq_max this hx.isSelfAdjoint, he.1.2, hx.norm_le, max_self]
     simp [← one_div, smul_add, smul_sub, ← two_smul ℝ, smul_smul, mul_one_div_cancel]
   · refine inter_extremePoints_subset_extremePoints_of_subset inter_subset_right
-      ⟨⟨he.1, ?_⟩, by simpa using Unitary.coe_mem_extremePoints_closedUnitBall ⟨e, he.2⟩⟩
+      ⟨⟨he.1, ?_⟩, by simpa using Unitary.coe_mem_extremePoints_unitClosedBall ⟨e, he.2⟩⟩
     nontriviality A
     simp [he]
 
 /-- An alternate statement for
-`mem_extremePoints_isSelfAdjoint_and_mem_closedUnitBall_iff_isSelfAdjoint_and_mem_unitary`. -/
-theorem selfAdjoint.mem_extremePoints_closedUnitBall_iff_coe_mem_unitary
+`mem_extremePoints_isSelfAdjoint_and_mem_unitClosedBall_iff_isSelfAdjoint_and_mem_unitary`. -/
+theorem selfAdjoint.mem_extremePoints_unitClosedBall_iff_coe_mem_unitary
     {A : Type*} [CStarAlgebra A] {e : selfAdjoint A} :
     e ∈ extremePoints ℝ (closedBall 0 1) ↔ (e : A) ∈ unitary A := by
   rw [show (e : A) ∈ unitary A ↔ (IsSelfAdjoint (e : A) ∧ (e : A) ∈ unitary A) by simp,
-    ← mem_extremePoints_isSelfAdjoint_and_mem_closedUnitBall_iff_isSelfAdjoint_and_mem_unitary]
+    ← mem_extremePoints_isSelfAdjoint_and_mem_unitClosedBall_iff_isSelfAdjoint_and_mem_unitary]
   simp [mem_extremePoints, selfAdjoint.mem_iff, ← isSelfAdjoint_iff]
   simp [Subtype.ext_iff, openSegment]

LeanOA/IsUnital.lean

@@ -0,0 +1,81 @@
+import Mathlib.Analysis.CStarAlgebra.Classes
+
+/-- A multiplicative magma is **unital** if there exists a unit.
+
+**Note**: Do not use this unless it is the only reasonable way to phrase or prove a statement.
+In general you should use `NonUnitalRing`, `Ring`, etc. -/
+@[mk_iff] class IsUnital (A : Type*) [Mul A] : Prop where
+  isUnital : ∃ u : A, ∀ x : A, u * x = x ∧ x * u = x
+
+/-- A multiplicative magma is **not-unital** if there does not exist a unit. -/
+@[mk_iff] class IsNotUnital (A : Type*) [Mul A] : Prop where
+  isNotUnital : ∀ u : A, ∃ x : A, u * x ≠ x ∨ x * u ≠ x
+
+@[simp] lemma not_isUnital_iff_isNotUnital {A : Type*} [Mul A] : ¬IsUnital A ↔ IsNotUnital A := by
+  simp [isUnital_iff, isNotUnital_iff, -not_and, not_and_or]
+
+@[simp] lemma not_isNotUnital_iff_isUnital {A : Type*} [Mul A] : ¬IsNotUnital A ↔ IsUnital A := by
+  grind [not_isUnital_iff_isNotUnital]
+
+variable {A : Type*}
+
+/-- A unital magma is `MulOneClass`. -/
+noncomputable abbrev IsUnital.toMulOneClass [Mul A] [IsUnital A] : MulOneClass A where
+  one := isUnital.choose
+  one_mul a := (isUnital.choose_spec a).1
+  mul_one a := (isUnital.choose_spec a).2
+
+lemma MulOneClass.isUnital [MulOneClass A] : IsUnital A where
+  isUnital := ⟨1, fun x ↦ ⟨one_mul x, mul_one x⟩⟩
+
+noncomputable section
+namespace IsUnital
+
+attribute [local instance] IsUnital.toMulOneClass
+
+/-- A unital semigroup is a monoid. -/
+abbrev toMonoid [Semigroup A] [IsUnital A] : Monoid A where
+
+/-- A unital non-associative semiring is a non-associative semiring. -/
+abbrev toNonAssocSemiring [NonUnitalNonAssocSemiring A] [IsUnital A] : NonAssocSemiring A where
+
+/-- A unital non-unital non-associative commutative semiring is a non-associative
+commutative semiring. -/
+abbrev toNonAssocCommSemiring [NonUnitalNonAssocCommSemiring A] [IsUnital A] :
+    NonAssocCommSemiring A where
+
+/-- A unital non-unital semiring is a semiring. -/
+abbrev toSemiring [NonUnitalSemiring A] [IsUnital A] : Semiring A where
+
+/-- A unital non-unital commutative semiring is a commutative semiring. -/
+abbrev toCommSemiring [NonUnitalCommSemiring A] [IsUnital A] : CommSemiring A where
+
+/-- A unital non-unital non-associative ring is a non-associative ring. -/
+abbrev toNonAssocRing [NonUnitalNonAssocRing A] [IsUnital A] : NonAssocRing A where
+
+/-- A unital non-unital non-associative commutative ring is a non-associative commutative ring. -/
+abbrev toNonAssocCommRing [NonUnitalNonAssocCommRing A] [IsUnital A] : NonAssocCommRing A where
+
+/-- A unital non-unital ring is a ring. -/
+abbrev toRing [NonUnitalRing A] [IsUnital A] : Ring A where
+
+/-- A unital non-unital commutative ring is a commutative ring. -/
+abbrev toCommRing [NonUnitalCommRing A] [IsUnital A] : CommRing A where
+
+attribute [local instance] IsUnital.toSemiring in
+/-- A unital non-unital algebra is an algebra. -/
+abbrev toAlgebra {R} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A]
+    [SMulCommClass R A A] [IsUnital A] : Algebra R A := .ofModule smul_mul_assoc mul_smul_comm
+
+/-- A unital non-unital C⋆-algebra is a C⋆-algebra. -/
+abbrev toCStarAlgebra [NonUnitalCStarAlgebra A] [IsUnital A] : CStarAlgebra A where
+  __ := ‹NonUnitalCStarAlgebra A›
+  __ := toSemiring
+  __ := toAlgebra
+
+attribute [local instance] IsUnital.toCStarAlgebra in
+/-- A unital non-unital commutative C⋆-algebra is a commutative C⋆-algebra. -/
+abbrev toCommCStarAlgebra [NonUnitalCommCStarAlgebra A] [IsUnital A] : CommCStarAlgebra A where
+
+end IsUnital
+end