Theorems · Definition · functional analysis

NonUnitalCStarAlgebra.mk.noConfusion

{A : Type u_1} →
  {P : Sort u} →
    {toNonUnitalNormedRing : NonUnitalNormedRing A} →
      {toStarRing : StarRing A} →
        {toCompleteSpace : CompleteSpace A} →
          {toCStarRing : CStarRing A} →
            {toNormedSpace : NormedSpace ℂ A} →
              {toIsScalarTower : IsScalarTower ℂ A A} →
                {toSMulCommClass : SMulCommClass ℂ A A} →
                  {toStarModule : StarModule ℂ A} →
                    {toNonUnitalNormedRing' : NonUnitalNormedRing A} →
                      {toStarRing' : StarRing A} →
                        {toCompleteSpace' : CompleteSpace A} →
                          {toCStarRing' : CStarRing A} →
                            {toNormedSpace' : NormedSpace ℂ A} →
                              {toIsScalarTower' : IsScalarTower ℂ A A} →
                                {toSMulCommClass' : SMulCommClass ℂ A A} →
                                  {toStarModule' : StarModule ℂ A} →
                                    { toNonUnitalNormedRing := toNonUnitalNormedRing, toStarRing := toStarRing,
                                          toCompleteSpace := toCompleteSpace, toCStarRing := toCStarRing,
                                          toNormedSpace := toNormedSpace, toIsScalarTower := toIsScalarTower,
                                          toSMulCommClass := toSMulCommClass, toStarModule := toStarModule } =
                                        { toNonUnitalNormedRing := toNonUnitalNormedRing', toStarRing := toStarRing',
                                          toCompleteSpace := toCompleteSpace', toCStarRing := toCStarRing',
                                          toNormedSpace := toNormedSpace', toIsScalarTower := toIsScalarTower',
                                          toSMulCommClass := toSMulCommClass', toStarModule := toStarModule' } →
                                      (toNonUnitalNormedRing ≍ toNonUnitalNormedRing' →
                                          toStarRing ≍ toStarRing' → toNormedSpace ≍ toNormedSpace' → P) →
                                        P

Defined in

Mathlib.Analysis.CStarAlgebra.Classes

Cited by

0 results in Mathlib

Foundations

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