Theorems · Definition · functional analysis

CStarAlgebra.recOn

{A : Type u_1} →
  {motive : CStarAlgebra A → Sort u} →
    (t : CStarAlgebra A) →
      ([toNormedRing : NormedRing A] →
          [toStarRing : StarRing A] →
            [toCompleteSpace : CompleteSpace A] →
              [toCStarRing : CStarRing A] →
                [toNormedAlgebra : NormedAlgebra ℂ A] →
                  [toStarModule : StarModule ℂ A] →
                    motive
                      { toNormedRing := toNormedRing, 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