Documentation Verification Report

Constructions

📁 Source: Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean

Statistics

Metric	Count
Definitions `instCStarModule`, `instCStarModuleComplex`, `instCStarModuleForall`, `instCStarModuleProd`, `instNormForall`, `instNormProd`, `instNormedAddCommGroupForall`, `instNormedAddCommGroupProd`, `instNormedSpaceComplexForall`, `instNormedSpaceComplexProd`, `normedAddCommGroupPiAux`, `normedAddCommGroupProdAux`	12
Theorems `inner_def`, `inner_single_left`, `inner_single_right`, `max_le_prod_norm`, `norm_apply_le_norm`, `norm_equiv_le_norm_pi`, `norm_equiv_le_norm_prod`, `norm_single`, `pi_inner`, `pi_norm`, `pi_norm_le_sum_norm`, `pi_norm_sq`, `prod_inner`, `prod_norm`, `prod_norm_le_norm_add`, `prod_norm_sq`	16
Total	28

WithCStarModule

Definitions

Name	Category	Theorems
`instCStarModule` 📖	CompOp	12 math math: `inner_def`, `CStarMatrix.toCLM_injective`, `CStarMatrix.norm_def'`, `CStarMatrix.inner_toCLM_conjTranspose_left`, `CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM`, `CStarMatrix.toCLM_apply_single`, `CStarMatrix.toCLM_apply_eq_sum`, `CStarMatrix.toCLM_apply`, `CStarMatrix.mul_entry_mul_eq_inner_toCLM`, `CStarMatrix.norm_def`, `CStarMatrix.inner_toCLM_conjTranspose_right`, `CStarMatrix.toCLM_apply_single_apply`
`instCStarModuleComplex` 📖	CompOp	—
`instCStarModuleForall` 📖	CompOp	6 math math: `CStarMatrix.inner_toCLM_conjTranspose_left`, `pi_inner`, `CStarMatrix.mul_entry_mul_eq_inner_toCLM`, `inner_single_right`, `inner_single_left`, `CStarMatrix.inner_toCLM_conjTranspose_right`
`instCStarModuleProd` 📖	CompOp	1 math math: `prod_inner`
`instNormForall` 📖	CompOp	12 math math: `CStarMatrix.inner_toCLM_conjTranspose_left`, `norm_apply_le_norm`, `pi_norm`, `pi_inner`, `norm_single`, `CStarMatrix.mul_entry_mul_eq_inner_toCLM`, `inner_single_right`, `pi_norm_le_sum_norm`, `norm_equiv_le_norm_pi`, `inner_single_left`, `pi_norm_sq`, `CStarMatrix.inner_toCLM_conjTranspose_right`
`instNormProd` 📖	CompOp	6 math math: `prod_norm_sq`, `prod_norm_le_norm_add`, `prod_norm`, `norm_equiv_le_norm_prod`, `max_le_prod_norm`, `prod_inner`
`instNormedAddCommGroupForall` 📖	CompOp	11 math math: `CStarMatrix.toCLM_injective`, `CStarMatrix.norm_def'`, `CStarMatrix.inner_toCLM_conjTranspose_left`, `CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM`, `CStarMatrix.toCLM_apply_single`, `CStarMatrix.toCLM_apply_eq_sum`, `CStarMatrix.toCLM_apply`, `CStarMatrix.mul_entry_mul_eq_inner_toCLM`, `CStarMatrix.norm_def`, `CStarMatrix.inner_toCLM_conjTranspose_right`, `CStarMatrix.toCLM_apply_single_apply`
`instNormedAddCommGroupProd` 📖	CompOp	—
`instNormedSpaceComplexForall` 📖	CompOp	3 math math: `CStarMatrix.norm_def'`, `CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM`, `CStarMatrix.norm_def`
`instNormedSpaceComplexProd` 📖	CompOp	—
`normedAddCommGroupPiAux` 📖	CompOp	—
`normedAddCommGroupProdAux` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inner_def` 📖	mathematical	—	`Inner.inner` `CStarModule.toInner` `NonUnitalRing.toNonUnitalSemiring` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `NonUnitalCStarAlgebra.toStarRing` `NormedSpace.toModule` `Complex` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNormedSpace` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNorm` `instCStarModule` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	—
`inner_single_left` 📖	mathematical	—	`Inner.inner` `WithCStarModule` `CStarModule.toInner` `NonUnitalRing.toNonUnitalSemiring` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `NonUnitalCStarAlgebra.toStarRing` `NormedSpace.toModule` `Complex` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNormedSpace` `instAddCommGroup` `Pi.addCommGroup` `NormedAddCommGroup.toAddCommGroup` `instModule` `Complex.instSemiring` `Pi.module` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instSMul` `Pi.instSMul` `NonUnitalNormedRing.toNorm` `instNormForall` `instCStarModuleForall` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equiv` `Pi.single` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toNorm`	—	`Finset.sum_congr` `Finset.sum_eq_single` `Pi.single_eq_of_ne` `CStarModule.inner_zero_left` `NonUnitalCStarAlgebra.toStarModule` `Pi.single_eq_same` `instIsEmptyFalse`
`inner_single_right` 📖	mathematical	—	`Inner.inner` `WithCStarModule` `CStarModule.toInner` `NonUnitalRing.toNonUnitalSemiring` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `NonUnitalCStarAlgebra.toStarRing` `NormedSpace.toModule` `Complex` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNormedSpace` `instAddCommGroup` `Pi.addCommGroup` `NormedAddCommGroup.toAddCommGroup` `instModule` `Complex.instSemiring` `Pi.module` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instSMul` `Pi.instSMul` `NonUnitalNormedRing.toNorm` `instNormForall` `instCStarModuleForall` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equiv` `Pi.single` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toNorm`	—	`Finset.sum_congr` `Finset.sum_eq_single` `Pi.single_eq_of_ne` `CStarModule.inner_zero_right` `NonUnitalCStarAlgebra.toStarModule` `Pi.single_eq_same` `instIsEmptyFalse`
`max_le_prod_norm` 📖	mathematical	—	`Real` `Real.instLE` `Real.instMax` `Norm.norm` `NormedAddCommGroup.toNorm` `WithCStarModule` `instNormProd`	—	`prod_norm` `CStarModule.norm_eq_sqrt_norm_inner_self` `CStarAlgebra.norm_le_norm_of_nonneg_of_le` `CStarModule.inner_self_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `StarOrderedRing.toIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `covariant_swap_add_of_covariant_add` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add`
`norm_apply_le_norm` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `WithCStarModule` `instNormForall`	—	`abs_le_of_sq_le_sq'` `Real.instIsStrictOrderedRing` `pi_norm_sq` `CStarModule.norm_sq_eq` `CStarAlgebra.norm_le_norm_of_nonneg_of_le` `CStarModule.inner_self_nonneg` `Finset.single_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedCancelAddMonoid.toIsOrderedAddMonoid` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `StarOrderedRing.toIsOrderedAddMonoid` `Finset.mem_univ` `norm_nonneg`
`norm_equiv_le_norm_pi` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `Pi.normedAddCommGroup` `DFunLike.coe` `Equiv` `WithCStarModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `instNormForall`	—	`pi_norm_le_iff_of_nonneg` `norm_nonneg` `norm_apply_le_norm`
`norm_equiv_le_norm_prod` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `Prod.toNorm` `NormedAddCommGroup.toNorm` `DFunLike.coe` `Equiv` `WithCStarModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `instNormProd`	—	`max_le_prod_norm`
`norm_single` 📖	mathematical	—	`Norm.norm` `WithCStarModule` `instNormForall` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equiv` `Pi.single` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toNorm`	—	`sq_eq_sq₀` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `norm_nonneg` `CStarModule.norm_sq_eq` `inner_single_right` `Pi.single_eq_same`
`pi_inner` 📖	mathematical	—	`Inner.inner` `WithCStarModule` `CStarModule.toInner` `NonUnitalRing.toNonUnitalSemiring` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `NonUnitalCStarAlgebra.toStarRing` `NormedSpace.toModule` `Complex` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNormedSpace` `instAddCommGroup` `Pi.addCommGroup` `NormedAddCommGroup.toAddCommGroup` `instModule` `Complex.instSemiring` `Pi.module` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instSMul` `Pi.instSMul` `NonUnitalNormedRing.toNorm` `instNormForall` `instCStarModuleForall` `Finset.sum` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNormedAddCommGroup` `Finset.univ` `NormedAddCommGroup.toNorm`	—	—
`pi_norm` 📖	mathematical	—	`Norm.norm` `WithCStarModule` `instNormForall` `Real.sqrt` `NonUnitalNormedRing.toNorm` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `Finset.univ` `Inner.inner` `CStarModule.toInner` `NonUnitalRing.toNonUnitalSemiring` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toStarRing` `NormedSpace.toModule` `Complex` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalCStarAlgebra.toNormedSpace` `NormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toNorm`	—	—
`pi_norm_le_sum_norm` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `WithCStarModule` `instNormForall` `Finset.sum` `Real.instAddCommMonoid` `Finset.univ` `NormedAddCommGroup.toNorm`	—	`abs_le_of_sq_le_sq'` `Real.instIsStrictOrderedRing` `norm_sum_le` `pi_norm_sq` `Finset.sum_congr` `CStarModule.norm_sq_eq` `Finset.sum_sq_le_sq_sum_of_nonneg` `Real.instIsOrderedRing` `norm_nonneg` `Finset.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`pi_norm_sq` 📖	mathematical	—	`Real` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `WithCStarModule` `instNormForall` `NonUnitalNormedRing.toNorm` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `Finset.univ` `Inner.inner` `CStarModule.toInner` `NonUnitalRing.toNonUnitalSemiring` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toStarRing` `NormedSpace.toModule` `Complex` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalCStarAlgebra.toNormedSpace` `NormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toNorm`	—	`pi_norm` `Real.sq_sqrt`
`prod_inner` 📖	mathematical	—	`Inner.inner` `WithCStarModule` `CStarModule.toInner` `NonUnitalRing.toNonUnitalSemiring` `NonUnitalNormedRing.toNonUnitalRing` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `NonUnitalCStarAlgebra.toStarRing` `NormedSpace.toModule` `Complex` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNormedSpace` `instAddCommGroup` `Prod.instAddCommGroup` `NormedAddCommGroup.toAddCommGroup` `instModule` `Complex.instSemiring` `Prod.instModule` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instSMul` `Prod.instSMul` `NonUnitalNormedRing.toNorm` `instNormProd` `instCStarModuleProd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NormedAddCommGroup.toNorm`	—	—
`prod_norm` 📖	mathematical	—	`Norm.norm` `WithCStarModule` `instNormProd` `Real.sqrt` `NonUnitalNormedRing.toNorm` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `Inner.inner` `CStarModule.toInner` `NonUnitalRing.toNonUnitalSemiring` `NonUnitalCStarAlgebra.toStarRing` `NormedSpace.toModule` `Complex` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNormedSpace` `NormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toNorm`	—	—
`prod_norm_le_norm_add` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `WithCStarModule` `instNormProd` `Real.instAdd` `NormedAddCommGroup.toNorm`	—	`abs_le_of_sq_le_sq'` `Real.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `norm_add_le` `prod_norm_sq` `CStarModule.norm_sq_eq` `add_zero` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `add_le_add_right` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `le_of_lt` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `norm_nonneg` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.pow_nat` `Mathlib.Tactic.Ring.coeff_one` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.pow_bit0` `Mathlib.Tactic.Ring.pow_one` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `add_nonneg`
`prod_norm_sq` 📖	mathematical	—	`Real` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `WithCStarModule` `instNormProd` `NonUnitalNormedRing.toNorm` `NonUnitalCStarAlgebra.toNonUnitalNormedRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `Inner.inner` `CStarModule.toInner` `NonUnitalRing.toNonUnitalSemiring` `NonUnitalCStarAlgebra.toStarRing` `NormedSpace.toModule` `Complex` `Complex.instNormedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NonUnitalCStarAlgebra.toNormedSpace` `NormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toNorm`	—	`Real.sq_sqrt`

---

← Back to Index