Theorems · Definition · functional analysis

NonUnitalCommCStarAlgebra.mk.noConfusion

{A : Type u_1} →
  {P : Sort u} →
    {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} →
                    {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} →
                                    { toNonUnitalNormedCommRing := toNonUnitalNormedCommRing, toStarRing := toStarRing,
                                          toCompleteSpace := toCompleteSpace, toCStarRing := toCStarRing,
                                          toNormedSpace := toNormedSpace, toIsScalarTower := toIsScalarTower,
                                          toSMulCommClass := toSMulCommClass, toStarModule := toStarModule } =
                                        { toNonUnitalNormedCommRing := toNonUnitalNormedCommRing',
                                          toStarRing := toStarRing', toCompleteSpace := toCompleteSpace',
                                          toCStarRing := toCStarRing', toNormedSpace := toNormedSpace',
                                          toIsScalarTower := toIsScalarTower', toSMulCommClass := toSMulCommClass',
                                          toStarModule := toStarModule' } →
                                      (toNonUnitalNormedCommRing ≍ toNonUnitalNormedCommRing' →
                                          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