Theorems · Definition · functional analysis

NonUnitalCommCStarAlgebra.casesOn

{A : Type u_1} →
  {motive : NonUnitalCommCStarAlgebra A → Sort u} →
    (t : NonUnitalCommCStarAlgebra A) →
      ([toNonUnitalNormedCommRing : NonUnitalNormedCommRing A] →
          [toStarRing : StarRing A] →
            [toCompleteSpace : CompleteSpace A] →
              [toCStarRing : CStarRing A] →
                [toNormedSpace : NormedSpace ℂ A] →
                  [toIsScalarTower : IsScalarTower ℂ A A] →
                    [toSMulCommClass : SMulCommClass ℂ A A] →
                      [toStarModule : StarModule ℂ A] →
                        motive
                          { toNonUnitalNormedCommRing := toNonUnitalNormedCommRing, toStarRing := toStarRing,
                            toCompleteSpace := toCompleteSpace, toCStarRing := toCStarRing,
                            toNormedSpace := toNormedSpace, toIsScalarTower := toIsScalarTower,
                            toSMulCommClass := toSMulCommClass, 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