Theorems · Definition · functional analysis

CommCStarAlgebra.casesOn

{A : Type u_1} →
  {motive : CommCStarAlgebra A → Sort u} →
    (t : CommCStarAlgebra A) →
      ([toNormedCommRing : NormedCommRing A] →
          [toStarRing : StarRing A] →
            [toCompleteSpace : CompleteSpace A] →
              [toCStarRing : CStarRing A] →
                [toNormedAlgebra : NormedAlgebra ℂ A] →
                  [toStarModule : StarModule ℂ A] →
                    motive
                      { toNormedCommRing := toNormedCommRing, toStarRing := toStarRing,
                        toCompleteSpace := toCompleteSpace, toCStarRing := toCStarRing,
                        toNormedAlgebra := toNormedAlgebra, toStarModule := toStarModule }) →
        motive t

Defined in

Mathlib.Analysis.CStarAlgebra.Classes

Cited by

0 results in Mathlib

Foundations

Depth 139 from the axioms · uses propext, Classical.choice, Quot.sound