Documentation Verification Report

Unitization

📁 Source: Mathlib/Analysis/CStarAlgebra/Unitization.lean

Statistics

Metric	Count
Definitions `«term_⁺¹»`, `instCStarAlgebra`, `instCommCStarAlgebra`	3
Theorems `instRegularNormedAlgebra`, `isometry_mul_flip`, `opNNNorm_mul_flip_apply`, `opNorm_mul_flip_apply`, `instCStarRing`, `norm_splitMul_snd_sq`	6
Total	9

CStarAlgebra

Definitions

Name	Category	Theorems
`«term_⁺¹»` 📖	CompOp	—

CStarRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instRegularNormedAlgebra` 📖	mathematical	—	`RegularNormedAlgebra` `DenselyNormedField.toNontriviallyNormedField` `NonUnitalNormedRing.toNonUnitalSeminormedRing`	—	`AddMonoidHomClass.isometry_of_norm` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomIsometric.ids` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `NNReal.eq_iff` `ContinuousLinearMap.sSup_unitClosedBall_eq_nnnorm` `csSup_eq_of_forall_le_of_forall_lt_exists_gt` `Set.Nonempty.image` `Metric.nonempty_closedBall` `zero_le_one` `Real.instZeroLEOneClass` `LE.le.trans` `ContinuousLinearMap.unit_le_opNorm` `mem_closedBall_zero_iff` `ContinuousLinearMap.opNorm_mul_apply_le` `LE.le.trans_lt` `zero_le'` `NormedField.exists_lt_nnnorm_lt` `mul_lt_mul_of_pos_right` `IsStrictOrderedRing.toMulPosStrictMono` `NNReal.instIsStrictOrderedRing` `NNReal.lt_inv_iff_mul_lt` `inv_ne_zero` `LT.lt.ne'` `inv_inv` `inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `norm_smul` `NormedSpace.toNormSMulClass` `norm_star` `to_normedStarGroup` `NNReal.le_inv_iff_mul_le` `LT.lt.le` `one_mul` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `nnnorm_smul` `nnnorm_self_mul_star` `div_lt_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `mul_pos` `div_eq_mul_inv` `mul_inv` `mul_assoc`

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isometry_mul_flip` 📖	mathematical	—	`Isometry` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NonUnitalNormedRing.toMetricSpace` `NormedRing.toMetricSpace` `toNormedRing` `NonUnitalNormedRing.toNormedAddCommGroup` `DFunLike.coe` `topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `module` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `funLike` `flip` `RingHomIsometric.ids` `mul`	—	`AddMonoidHomClass.isometry_of_norm` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomIsometric.ids` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `continuousSemilinearMapClass` `opNorm_mul_flip_apply`
`opNNNorm_mul_flip_apply` 📖	mathematical	—	`NNNorm.nnnorm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DFunLike.coe` `topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddGroup.toAddGroup` `module` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `funLike` `flip` `mul`	—	`RingHomIsometric.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `opNorm_mul_flip_apply`
`opNorm_mul_flip_apply` 📖	mathematical	—	`Norm.norm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `hasOpNorm` `DFunLike.coe` `topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `module` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `funLike` `flip` `RingHomIsometric.ids` `mul` `NonUnitalNormedRing.toNorm`	—	`le_antisymm` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomIsometric.ids` `opNorm_le_bound` `norm_nonneg` `mul_comm` `norm_mul_le` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `StarMul.star_mul` `star_star` `norm_star` `le_opNorm` `opNorm_mul_apply`

Unitization

Definitions

Name	Category	Theorems
`instCStarAlgebra` 📖	CompOp	4 math math: `real_cfcₙ_eq_cfc_inr`, `inr_comp_cfcₙHom_eq_cfcₙAux`, `nnreal_cfcₙ_eq_cfc_inr`, `complex_cfcₙ_eq_cfc_inr`
`instCommCStarAlgebra` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCStarRing` 📖	mathematical	—	`CStarRing` `Unitization` `NormedRing.toNonUnitalNormedRing` `instNormedRing` `DenselyNormedField.toNontriviallyNormedField` `CStarRing.instRegularNormedAlgebra` `instStarRing` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing`	—	`CStarRing.instRegularNormedAlgebra` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `IsScalarTower.left` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `splitMul_apply` `norm_zero` `RingHomIsometric.ids` `norm_nonneg` `LE.le.trans` `norm_splitMul_snd_sq` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Prod.snd_mul` `norm_mul_le` `mul_le_mul_iff_left₀` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `norm_pos_iff` `sq` `le_antisymm` `mul_le_mul_of_nonneg_right` `star_star` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_star` `CStarRing.to_normedStarGroup` `sup_eq_right` `mul_self_le_mul_self` `IsOrderedRing.toPosMulMono` `le_refl` `LT.lt.le` `sup_eq_left`
`norm_splitMul_snd_sq` 📖	mathematical	—	`Real` `Real.instLE` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `ContinuousLinearMap.hasOpNorm` `DFunLike.coe` `AlgHom` `Unitization` `Semifield.toCommSemiring` `instSemiring` `NonUnitalRing.toNonUnitalSemiring` `NonUnitalNormedRing.toNonUnitalRing` `Prod.instSemiring` `ContinuousLinearMap.semiring` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `instAlgebra` `Algebra.id` `Module.toDistribMulAction` `CommSemiring.toSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Prod.algebra` `ContinuousLinearMap.algebra` `SeminormedAddCommGroup.toAddCommGroup` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `AddCommGroup.toAddCommMonoid` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toIsBoundedSMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `AlgHom.funLike` `splitMul` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DenselyNormedField.toNormedField` `Distrib.toAdd` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `Star.star` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	`RingHomIsometric.ids` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `IsScalarTower.left` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Real.le_sqrt` `norm_nonneg` `splitMul_apply` `ContinuousLinearMap.sSup_unitClosedBall_eq_norm` `csSup_le` `Set.Nonempty.image` `Metric.nonempty_closedBall` `zero_le_one` `Real.instZeroLEOneClass` `Real.sqrt_sq` `Real.sqrt_le_sqrt_iff` `sq` `CStarRing.norm_star_mul_self` `ContinuousLinearMap.add_apply` `StarAddMonoid.star_add` `ContinuousLinearMap.mul_apply'` `Algebra.algebraMap_eq_smul_one` `ContinuousLinearMap.smul_apply` `ContinuousLinearMap.one_apply` `StarMul.star_mul` `StarModule.star_smul` `add_mul` `Distrib.rightDistribClass` `smul_mul_assoc` `mul_smul_comm` `mul_assoc` `mul_add` `Distrib.leftDistribClass` `LE.le.trans` `norm_mul_le` `one_mul` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `mem_closedBall_zero_iff` `norm_star` `CStarRing.to_normedStarGroup` `le_csSup` `norm_add_le` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Eq.trans_le` `norm_smul` `NormedSpace.toNormSMulClass` `mul_one` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `ContinuousLinearMap.unit_le_opNorm` `ContinuousLinearMap.opNorm_mul_apply_le` `smul_add` `smul_smul`

---

← Back to Index