Documentation Verification Report

SingularValues

📁 Source: Mathlib/Analysis/InnerProductSpace/SingularValues.lean

Statistics

Metric	Count
Definitions `singularValues`	1
Theorems `card_support_singularValues`, `hasEigenvalue_adjoint_comp_self_sq_singularValues`, `injective_iff_forall_lt_finrank_singularValues_pos`, `isLowerSet_support_singularValues`, `singularValues_antitone`, `singularValues_eq_zero_iff`, `singularValues_eq_zero_iff_le_finrank_range`, `singularValues_fin`, `singularValues_finrank_range_self`, `singularValues_nonneg`, `singularValues_of_finrank_le`, `singularValues_of_lt`, `singularValues_pos_iff_lt_finrank_range`, `singularValues_pos_iff_ne_zero`, `singularValues_zero`, `sq_singularValues_fin`, `sq_singularValues_of_lt`, `support_singularValues`	18
Total	19

LinearMap

Definitions

Name	Category	Theorems
`singularValues` 📖	CompOp	18 math math: `singularValues_zero`, `singularValues_antitone`, `isLowerSet_support_singularValues`, `singularValues_nonneg`, `singularValues_eq_zero_iff`, `injective_iff_forall_lt_finrank_singularValues_pos`, `hasEigenvalue_adjoint_comp_self_sq_singularValues`, `singularValues_pos_iff_lt_finrank_range`, `singularValues_fin`, `sq_singularValues_of_lt`, `sq_singularValues_fin`, `singularValues_of_finrank_le`, `singularValues_finrank_range_self`, `singularValues_pos_iff_ne_zero`, `support_singularValues`, `singularValues_of_lt`, `singularValues_eq_zero_iff_le_finrank_range`, `card_support_singularValues`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_support_singularValues` 📖	mathematical	—	`Finset.card` `Finsupp.support` `Real` `Real.instZero` `singularValues` `Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `SetLike.instMembership` `Submodule.setLike` `range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.addCommMonoid` `Submodule.module`	—	`RingHomCompTriple.ids` `RingHomInvPair.instStarRingEnd` `smulCommClass_self` `isSymmetric_adjoint_comp_self` `Finset.ext` `singularValues_fin` `IsPositive.isSymmetric` `isPositive_adjoint_comp_self` `IsPositive.nonneg_eigenvalues` `Finset.filter.congr_simp` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Finset.compl_filter` `RingHomSurjective.ids` `Finset.card_attachFin` `Finset.card_compl` `Fintype.card_fin` `IsSymmetric.card_filter_eigenvalues_eq` `Module.End.eigenspace_zero` `finrank_range_add_finrank_ker` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `range_adjoint_comp_self` `finrank_range_adjoint`
`hasEigenvalue_adjoint_comp_self_sq_singularValues` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace`	`Module.End.HasEigenvalue` `Field.toCommRing` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `DFunLike.coe` `LinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `starRingEnd` `Semifield.toCommSemiring` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `LinearMap` `addCommMonoid` `module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `adjoint` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `RCLike.ofReal` `Finsupp` `Real` `Real.instZero` `Finsupp.instFunLike` `singularValues`	—	`RingHomCompTriple.ids` `RingHomInvPair.instStarRingEnd` `smulCommClass_self` `isSymmetric_adjoint_comp_self` `sq_singularValues_fin` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsSymmetric.hasEigenvalue_eigenvalues`
`injective_iff_forall_lt_finrank_singularValues_pos` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `instFunLike` `Real` `Real.instLT` `Real.instZero` `Finsupp` `Finsupp.instFunLike` `singularValues`	—	`RingHomCompTriple.ids` `RingHomInvPair.instStarRingEnd` `smulCommClass_self` `List.TFAE.out` `IsScalarTower.left` `Module.Free.of_divisionRing` `not_hasEigenvalue_zero_tfae` `adjoint_comp_self_injective_iff` `coe_comp` `ker_eq_bot` `not_iff_not` `Iff.not_left` `Mathlib.Tactic.Push.not_forall_eq` `isSymmetric_adjoint_comp_self` `IsSymmetric.exists_eigenvalues_eq` `singularValues_fin` `RCLike.ofReal_eq_zero` `Real.sqrt_zero` `instReflLe` `sq_singularValues_of_lt` `le_antisymm` `singularValues_nonneg` `zero_pow` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsSymmetric.hasEigenvalue_eigenvalues`
`isLowerSet_support_singularValues` 📖	mathematical	—	`IsLowerSet` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support` `Real` `Real.instZero` `singularValues`	—	`Finset.mem_coe` `Finsupp.mem_support_iff` `singularValues_pos_iff_ne_zero` `ne_of_lt` `le_antisymm` `le_trans` `le_of_lt` `le_refl` `singularValues_antitone`
`singularValues_antitone` 📖	mathematical	—	`Antitone` `Real` `Nat.instPreorder` `Real.instPreorder` `DFunLike.coe` `Finsupp` `Real.instZero` `Finsupp.instFunLike` `singularValues`	—	`singularValues_of_finrank_le` `singularValues_nonneg` `RingHomCompTriple.ids` `RingHomInvPair.instStarRingEnd` `smulCommClass_self` `isSymmetric_adjoint_comp_self` `sq_singularValues_fin` `LE.le.trans_lt` `IsSymmetric.eigenvalues_antitone` `le_of_sq_le_sq` `Real.instIsStrictOrderedRing`
`singularValues_eq_zero_iff` 📖	mathematical	—	`singularValues` `Finsupp` `Real` `Real.instZero` `Finsupp.instZero` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `instZero`	—	`RingHomSurjective.ids` `range_eq_bot` `Submodule.finrank_eq_zero` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `finiteDimensional_range` `singularValues_eq_zero_iff_le_finrank_range` `Finsupp.zero_apply` `singularValues_zero`
`singularValues_eq_zero_iff_le_finrank_range` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `Real` `Real.instZero` `Finsupp.instFunLike` `singularValues` `Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `SetLike.instMembership` `Submodule.setLike` `range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.addCommMonoid` `Submodule.module`	—	`RingHomSurjective.ids` `Finsupp.notMem_support_iff` `support_singularValues` `Finset.mem_range` `not_lt`
`singularValues_fin` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace`	`DFunLike.coe` `Finsupp` `Real` `Real.instZero` `Finsupp.instFunLike` `singularValues` `Real.sqrt` `IsSymmetric.eigenvalues` `comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearEquiv` `starRingEnd` `Semifield.toCommSemiring` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `LinearMap` `addCommMonoid` `module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `adjoint` `isSymmetric_adjoint_comp_self`	—	`RingHomCompTriple.ids` `RingHomInvPair.instStarRingEnd` `smulCommClass_self` `isSymmetric_adjoint_comp_self` `Finsupp.embDomain_apply_self`
`singularValues_finrank_range_self` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `Real` `Real.instZero` `Finsupp.instFunLike` `singularValues` `Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `SetLike.instMembership` `Submodule.setLike` `range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.addCommMonoid` `Submodule.module`	—	`RingHomSurjective.ids` `Finsupp.notMem_support_iff` `support_singularValues` `Finset.notMem_range_self`
`singularValues_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `DFunLike.coe` `Finsupp` `Finsupp.instFunLike` `singularValues`	—	`isSymmetric_adjoint_comp_self` `Finsupp.embDomain_apply` `Finsupp.ofSupportFinite_coe` `Real.sqrt_nonneg` `Mathlib.Meta.Positivity.nonneg_of_isNat` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero`
`singularValues_of_finrank_le` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace`	`DFunLike.coe` `Finsupp` `Real` `Real.instZero` `Finsupp.instFunLike` `singularValues`	—	`Finsupp.embDomain_notin_range` `isSymmetric_adjoint_comp_self` `Fin.range_val`
`singularValues_of_lt` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace`	`DFunLike.coe` `Finsupp` `Real` `Real.instZero` `Finsupp.instFunLike` `singularValues` `Real.sqrt` `IsSymmetric.eigenvalues` `comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearEquiv` `starRingEnd` `Semifield.toCommSemiring` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `LinearMap` `addCommMonoid` `module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `adjoint` `isSymmetric_adjoint_comp_self`	—	`singularValues_fin`
`singularValues_pos_iff_lt_finrank_range` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `DFunLike.coe` `Finsupp` `Finsupp.instFunLike` `singularValues` `Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `SetLike.instMembership` `Submodule.setLike` `range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.addCommMonoid` `Submodule.module`	—	`RingHomSurjective.ids` `singularValues_pos_iff_ne_zero` `Finsupp.mem_support_iff` `support_singularValues` `Finset.mem_range`
`singularValues_pos_iff_ne_zero` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `DFunLike.coe` `Finsupp` `Finsupp.instFunLike` `singularValues`	—	—
`singularValues_zero` 📖	mathematical	—	`singularValues` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `instZero` `Finsupp` `Real` `Real.instZero` `Finsupp.instZero`	—	`Finsupp.ext` `Finsupp.zero_apply` `RingHomSurjective.ids` `singularValues_eq_zero_iff_le_finrank_range` `range_zero` `Module.finrank_eq_zero_of_subsingleton` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing` `finiteDimensional_bot` `Unique.instSubsingleton` `Nat.instCanonicallyOrderedAdd`
`sq_singularValues_fin` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace`	`Real` `Monoid.toPow` `Real.instMonoid` `DFunLike.coe` `Finsupp` `Real.instZero` `Finsupp.instFunLike` `singularValues` `IsSymmetric.eigenvalues` `comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearEquiv` `starRingEnd` `Semifield.toCommSemiring` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `LinearMap` `addCommMonoid` `module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `adjoint` `isSymmetric_adjoint_comp_self`	—	`RingHomCompTriple.ids` `RingHomInvPair.instStarRingEnd` `smulCommClass_self` `isSymmetric_adjoint_comp_self` `singularValues_fin` `Real.sq_sqrt` `IsPositive.nonneg_eigenvalues` `isPositive_adjoint_comp_self`
`sq_singularValues_of_lt` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace`	`Real` `Monoid.toPow` `Real.instMonoid` `DFunLike.coe` `Finsupp` `Real.instZero` `Finsupp.instFunLike` `singularValues` `IsSymmetric.eigenvalues` `comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `LinearEquiv` `starRingEnd` `Semifield.toCommSemiring` `RCLike.toStarRing` `RingHomInvPair.instStarRingEnd` `LinearMap` `addCommMonoid` `module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `adjoint` `isSymmetric_adjoint_comp_self`	—	`sq_singularValues_fin`
`support_singularValues` 📖	mathematical	—	`Finsupp.support` `Real` `Real.instZero` `singularValues` `Finset.range` `Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `SetLike.instMembership` `Submodule.setLike` `range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.addCommMonoid` `Submodule.module`	—	`RingHomSurjective.ids` `IsLowerSet.eq_univ_or_Iio` `instWellFoundedLTNat` `isLowerSet_support_singularValues` `Set.Infinite.not_finite` `Set.infinite_univ` `instInfiniteNat` `Finset.finite_toSet` `Nat.Iio_eq_range` `Finset.coe_Iio` `Finset.card_range`

---

← Back to Index