Documentation Verification Report

Span

📁 Source: Mathlib/Analysis/CStarAlgebra/Unitary/Span.lean

Statistics

Metric	Count
Definitions `unitarySelfAddISMul`	1
Theorems `exists_sum_four_unitary`, `norm_smul_two_inv_smul_add_four_unitary`, `span_unitary`, `self_add_I_smul_cfcSqrt_sub_sq_mem_unitary`, `realPart_unitarySelfAddISMul`, `star_coe_unitarySelfAddISMul`, `unitarySelfAddISMul_coe`	7
Total	8

CStarAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_sum_four_unitary` 📖	mathematical	—	`Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `toNormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `toNonUnitalCStarAlgebra` `Finset.univ` `Fin.fintype` `Complex` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Complex.instNormedField` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `toNormedAlgebra` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NormedRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `toStarRing` `Real` `Real.instLE` `Norm.norm` `Complex.instNorm` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `NormedRing.toNorm` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`spectralOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `eq_or_ne` `Finset.sum_congr` `zero_smul` `Finset.sum_const_zero` `norm_zero` `zero_div` `instTrivialStarReal` `StarModule.complexToReal` `toStarModule` `norm_smul_two_inv_smul_add_four_unitary` `smul_add` `Complex.ofReal_inv` `Fin.sum_univ_four` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.add_eq_eval₁` `zero_add` `Mathlib.Tactic.Module.NF.eq_cons_cons` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.inv_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Complex.instCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Fintype.complete` `Complex.norm_mul` `Complex.norm_real` `norm_norm` `norm_inv` `Complex.norm_ofNat` `div_eq_mul_inv` `Complex.norm_I` `mul_one`
`norm_smul_two_inv_smul_add_four_unitary` 📖	mathematical	—	`Real` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Real.normedField` `Ring.toSemiring` `SeminormedRing.toRing` `NormedRing.toSeminormedRing` `toNormedRing` `NormedAlgebra.toAlgebra` `NormedAlgebra.complexToReal` `toNormedAlgebra` `Norm.norm` `NormedRing.toNorm` `Real.instInv` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `toStarRing` `selfAdjoint.unitarySelfAddISMul` `DFunLike.coe` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddSubgroup` `AddCommGroup.toAddGroup` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `toNonUnitalCStarAlgebra` `AddSubgroup.instSetLike` `selfAdjoint` `StarRing.toStarAddMonoid` `AddCommGroup.toAddCommMonoid` `AddSubgroup.toAddCommGroup` `Module.complexToReal` `NormedSpace.toModule` `Complex` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNormedSpace` `selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Real.commRing` `instStarRingReal` `instTrivialStarReal` `StarModule.complexToReal` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toStarModule` `LinearMap.instFunLike` `realPart` `Star.star` `Unitary.instStarSubtypeMemSubmonoidUnitary` `Complex.I` `imaginaryPart`	—	`instTrivialStarReal` `StarModule.complexToReal` `toStarModule` `Nat.instAtLeastTwoHAddOfNat` `smul_add` `SMulCommClass.smul_comm` `SMulCommClass.complexToReal` `smulCommClass_self` `Unitary.coe_star` `realPart_apply_coe` `selfAdjoint.realPart_unitarySelfAddISMul` `realPart_add_I_smul_imaginaryPart` `NormedSpace.norm_smul_normalize`
`span_unitary` 📖	mathematical	—	`Submodule.span` `Complex` `Complex.instSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `toNormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `toNonUnitalCStarAlgebra` `NormedSpace.toModule` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNormedSpace` `SetLike.coe` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `toStarRing` `Top.top` `Submodule` `Submodule.instTop`	—	`eq_top_iff` `Nat.instAtLeastTwoHAddOfNat` `exists_sum_four_unitary` `sum_mem` `Submodule.addSubmonoidClass` `Submodule.smul_mem` `Submodule.subset_span`

IsSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`self_add_I_smul_cfcSqrt_sub_sq_mem_unitary` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `CStarAlgebra.toNormedRing` `StarRing.toStarAddMonoid` `CStarAlgebra.toStarRing` `Real` `Real.instLE` `Norm.norm` `NormedRing.toNorm` `Real.instOne`	`Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Complex` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Complex.instNormedField` `SeminormedRing.toRing` `NormedRing.toSeminormedRing` `NormedAlgebra.toAlgebra` `CStarAlgebra.toNormedAlgebra` `Complex.I` `CFC.sqrt` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `CStarAlgebra.toNonUnitalCStarAlgebra` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedSpace.complexToReal` `NonUnitalCStarAlgebra.toNormedSpace` `Algebra.to_smulCommClass` `NormedAlgebra.complexToReal` `IsScalarTower.right` `instNonUnitalContinuousFunctionalCalculus` `IsStarNormal.instNonUnitalContinuousFunctionalCalculus` `CStarAlgebra.instNonnegSpectrumClass'` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Monoid.toNatPow`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `instNonUnitalContinuousFunctionalCalculus` `IsStarNormal.instNonUnitalContinuousFunctionalCalculus` `CStarAlgebra.instNonnegSpectrumClass'` `subsingleton_or_nontrivial` `OneMemClass.one_mem` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.instContinuousStar` `IsStarNormal.instContinuousFunctionalCalculus` `Real.instNontrivial` `instIsTopologicalRingReal` `instContinuousStarReal` `CFC.sqrt_eq_real_sqrt` `NonUnitalSeminormedRing.toIsTopologicalRing` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `StarOrderedRing.toIsOrderedAddMonoid` `CStarAlgebra.norm_le_one_iff_of_nonneg` `sq_nonneg` `sq` `norm_mul_self` `CStarAlgebra.toCStarRing` `sq_le_one_iff₀` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instZeroLEOneClass` `norm_nonneg` `cfc_add` `Continuous.comp_continuousOn'` `Complex.continuous_ofReal` `Continuous.continuousOn` `Complex.continuous_re` `ContinuousOn.fun_mul` `IsTopologicalSemiring.toContinuousMul` `continuousOn_const` `ContinuousOn.sqrt` `ContinuousOn.sub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `Continuous.pow` `continuous_id'` `cfc_const_mul` `instContinuousFunctionalCalculus` `cfc_real_eq_complex` `cfc_id'` `IsDomain.toNontrivial` `instIsDomain` `ContinuousFunctionalCalculus.toNonUnital` `Real.instCompleteSpace` `cfcₙ_eq_cfc` `RCLike.uniqueNonUnitalContinuousFunctionalCalculus` `continuousOn_id'` `Real.sqrt_zero` `cfc_comp'` `Real.instContinuousMapUniqueHom` `ContinuousOn.pow` `cfc_sub` `cfc_pow` `cfc_const_one` `cfc_unitary_iff` `isStarNormal` `ContinuousOn.fun_add` `IsTopologicalSemiring.toContinuousAdd` `starRingEnd_apply` `Complex.normSq_eq_conj_mul_self` `Complex.normSq_ofReal_add_I_mul_sqrt_one_sub` `LE.le.trans` `spectrum.norm_le_norm_of_mem` `CStarAlgebra.toCompleteSpace` `CStarRing.instNormOneClassOfNontrivial` `SpectrumRestricts.apply_mem` `IsScalarTower.complexToReal` `IsScalarTower.left` `spectrumRestricts` `Complex.ofReal_one`

selfAdjoint

Definitions

Name	Category	Theorems
`unitarySelfAddISMul` 📖	CompOp	4 math math: `unitarySelfAddISMul_coe`, `CStarAlgebra.norm_smul_two_inv_smul_add_four_unitary`, `realPart_unitarySelfAddISMul`, `star_coe_unitarySelfAddISMul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`realPart_unitarySelfAddISMul` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `AddSubgroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `CStarAlgebra.toNonUnitalCStarAlgebra` `SetLike.instMembership` `AddSubgroup.instSetLike` `selfAdjoint` `StarRing.toStarAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `CStarAlgebra.toNormedRing` `CStarAlgebra.toStarRing` `NormedAddCommGroup.toNorm` `AddSubgroup.normedAddCommGroup` `Real.instOne`	`DFunLike.coe` `LinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddGroup` `NormedAddCommGroup.toAddCommGroup` `AddCommGroup.toAddCommMonoid` `AddSubgroup.toAddCommGroup` `Module.complexToReal` `NormedSpace.toModule` `Complex` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNormedSpace` `instModuleSubtypeMemAddSubgroupOfStarModule` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Real.commRing` `instStarRingReal` `instTrivialStarReal` `StarModule.complexToReal` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `CStarAlgebra.toStarModule` `LinearMap.instFunLike` `realPart` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `unitarySelfAddISMul`	—	`instTrivialStarReal` `StarModule.complexToReal` `CStarAlgebra.toStarModule` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `realPart_coe` `realPart_I_smul` `IsSelfAdjoint.imaginaryPart` `Algebra.to_smulCommClass` `IsScalarTower.right` `IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus` `IsStarNormal.instNonUnitalContinuousFunctionalCalculus` `CStarAlgebra.instNonnegSpectrumClass'` `IsSelfAdjoint.of_nonneg` `neg_zero` `add_zero`
`star_coe_unitarySelfAddISMul` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `AddSubgroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `CStarAlgebra.toNonUnitalCStarAlgebra` `SetLike.instMembership` `AddSubgroup.instSetLike` `selfAdjoint` `StarRing.toStarAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `CStarAlgebra.toNormedRing` `CStarAlgebra.toStarRing` `NormedAddCommGroup.toNorm` `AddSubgroup.normedAddCommGroup` `Real.instOne`	`Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `unitarySelfAddISMul` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `Complex` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Complex.instNormedField` `SeminormedRing.toRing` `NormedRing.toSeminormedRing` `NormedAlgebra.toAlgebra` `CStarAlgebra.toNormedAlgebra` `Complex.I` `CFC.sqrt` `NonUnitalNormedRing.toNonUnitalRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedSpace.complexToReal` `NonUnitalCStarAlgebra.toNormedSpace` `Algebra.to_smulCommClass` `NormedAlgebra.complexToReal` `IsScalarTower.right` `IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus` `IsStarNormal.instNonUnitalContinuousFunctionalCalculus` `CStarAlgebra.instNonnegSpectrumClass'` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Monoid.toNatPow`	—	`Algebra.to_smulCommClass` `IsScalarTower.right` `IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus` `IsStarNormal.instNonUnitalContinuousFunctionalCalculus` `CStarAlgebra.instNonnegSpectrumClass'` `StarAddMonoid.star_add` `IsSelfAdjoint.star_eq` `StarModule.star_smul` `CStarAlgebra.toStarModule` `Complex.conj_I` `LE.le.isSelfAdjoint` `CFC.sqrt_nonneg` `neg_smul`
`unitarySelfAddISMul_coe` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `AddSubgroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `CStarAlgebra.toNonUnitalCStarAlgebra` `SetLike.instMembership` `AddSubgroup.instSetLike` `selfAdjoint` `StarRing.toStarAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `CStarAlgebra.toNormedRing` `CStarAlgebra.toStarRing` `NormedAddCommGroup.toNorm` `AddSubgroup.normedAddCommGroup` `Real.instOne`	`Submonoid` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Submonoid.instSetLike` `unitary` `StarRing.toStarMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `unitarySelfAddISMul` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Complex` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Complex.instNormedField` `SeminormedRing.toRing` `NormedRing.toSeminormedRing` `NormedAlgebra.toAlgebra` `CStarAlgebra.toNormedAlgebra` `Complex.I` `CFC.sqrt` `NonUnitalNormedRing.toNonUnitalRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedSpace.complexToReal` `NonUnitalCStarAlgebra.toNormedSpace` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Monoid.toNatPow`	—	—

---

← Back to Index