Documentation Verification Report

Rayleigh

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

Statistics

Metric	Count
Definitions `rayleighQuotient`	1
Theorems `bddAbove_rayleighQuotient`, `iInf_rayleigh_eq_iInf_rayleigh_sphere`, `iSup_rayleigh_eq_iSup_rayleigh_sphere`, `image_rayleigh_eq_image_rayleigh_sphere`, `rayleighQuotient_add`, `rayleighQuotient_le_norm`, `rayleigh_smul`, `eq_smul_self_of_isLocalExtrOn`, `eq_smul_self_of_isLocalExtrOn_real`, `hasEigenvector_of_isLocalExtrOn`, `hasEigenvector_of_isMaxOn`, `hasEigenvector_of_isMinOn`, `linearly_dependent_of_isLocalExtrOn`, `hasEigenvalue_iInf_of_finiteDimensional`, `hasEigenvalue_iSup_of_finiteDimensional`, `hasStrictFDerivAt_reApplyInnerSelf`, `subsingleton_of_no_eigenvalue_finiteDimensional`	17
Total	18

ContinuousLinearMap

Definitions

Name	Category	Theorems
`rayleighQuotient` 📖	CompOp	12 math math: `rayleigh_smul`, `iSup_rayleigh_eq_iSup_rayleigh_sphere`, `image_rayleigh_eq_image_rayleigh_sphere`, `iInf_rayleigh_eq_iInf_rayleigh_sphere`, `IsSelfAdjoint.hasEigenvector_of_isMaxOn`, `IsSelfAdjoint.eq_smul_self_of_isLocalExtrOn_real`, `rayleighQuotient_add`, `rayleighQuotient_le_norm`, `IsSelfAdjoint.hasEigenvector_of_isMinOn`, `IsSelfAdjoint.hasEigenvector_of_isLocalExtrOn`, `bddAbove_rayleighQuotient`, `IsSelfAdjoint.eq_smul_self_of_isLocalExtrOn`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bddAbove_rayleighQuotient` 📖	mathematical	—	`BddAbove` `Real` `Real.instLE` `Set.range` `abs` `Real.lattice` `Real.instAddGroup` `rayleighQuotient`	—	`rayleighQuotient_le_norm`
`iInf_rayleigh_eq_iInf_rayleigh_sphere` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`iInf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.instInfSet` `rayleighQuotient` `Set.Elem` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instMembership`	—	`sInf_image'` `image_rayleigh_eq_image_rayleigh_sphere`
`iSup_rayleigh_eq_iSup_rayleigh_sphere` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`iSup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.instSupSet` `rayleighQuotient` `Set.Elem` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instMembership`	—	`sSup_image'` `image_rayleigh_eq_image_rayleigh_sphere`
`image_rayleigh_eq_image_rayleigh_sphere` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Set.image` `rayleighQuotient` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Metric.sphere` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`Set.ext` `map_inv₀` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `LT.lt.ne'` `sub_zero` `norm_smul` `NormedSpace.toNormSMulClass` `norm_mul` `norm_inv` `norm_algebraMap'` `NormedDivisionRing.to_normOneClass` `norm_norm` `abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `one_mul` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `norm_pos_iff` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `rayleigh_smul` `ne_zero_of_mem_sphere`
`rayleighQuotient_add` 📖	mathematical	—	`rayleighQuotient` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `add` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Real` `Real.instAdd`	—	`IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `inner_add_left` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `add_div`
`rayleighQuotient_le_norm` 📖	mathematical	—	`Real` `Real.instLE` `abs` `Real.lattice` `Real.instAddGroup` `rayleighQuotient` `Norm.norm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `hasOpNorm` `DenselyNormedField.toNontriviallyNormedField`	—	`rayleighQuotient.eq_1` `reApplyInnerSelf_apply` `abs_div` `Real.instIsStrictOrderedRing` `abs_sq` `Real.instIsOrderedRing` `le_imp_le_of_le_of_le` `div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `RCLike.abs_re_le_norm` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `AddGroup.existsAddOfLE` `Nat.instAtLeastTwoHAddOfNat` `even_two_mul` `le_refl` `norm_inner_le_norm` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `le_opNorm` `RingHomIsometric.ids` `norm_nonneg` `mul_assoc` `sq` `mul_div_assoc` `mul_le_of_le_one_right` `IsOrderedRing.toPosMulMono` `opNorm_nonneg` `div_self_le_one` `Real.instZeroLEOneClass`
`rayleigh_smul` 📖	mathematical	—	`rayleighQuotient` `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` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace`	—	`smul_zero` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `ne_of_gt` `norm_pos_iff` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.zpow'_ofNat` `norm_smul` `NormedSpace.toNormSMulClass` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `reApplyInnerSelf_smul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁`

IsSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_smul_self_of_isLocalExtrOn` 📖	mathematical	`IsSelfAdjoint` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.instStarId` `IsLocalExtrOn` `Real` `Real.instPreorder` `ContinuousLinearMap.reApplyInnerSelf` `Metric.sphere` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Norm.norm` `NormedAddCommGroup.toNorm`	`DFunLike.coe` `ContinuousLinearMap.funLike` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `RCLike.ofReal` `ContinuousLinearMap.rayleighQuotient`	—	`RingHomIsometric.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `LinearMap.IsScalarTower.compatibleSMul` `RestrictScalars.isScalarTower` `LinearMap.IsSymmetric.restrictScalars` `isSymmetric` `Subtype.prop` `eq_smul_self_of_isLocalExtrOn_real`
`eq_smul_self_of_isLocalExtrOn_real` 📖	mathematical	`IsSelfAdjoint` `ContinuousLinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `ContinuousLinearMap.instStarId` `IsLocalExtrOn` `Real.instPreorder` `ContinuousLinearMap.reApplyInnerSelf` `Metric.sphere` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Norm.norm` `NormedAddCommGroup.toNorm`	`DFunLike.coe` `ContinuousLinearMap.funLike` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `ContinuousLinearMap.rayleighQuotient`	—	`linearly_dependent_of_isLocalExtrOn` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `smul_zero` `smul_right_injective` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `Real.instIsDomain` `GroupWithZero.toNoZeroSMulDivisors` `IsDomain.toIsCancelMulZero` `zero_smul` `add_zero` `Mathlib.Tactic.LinearCombination.eq_of_eq` `AddRightCancelSemigroup.toIsRightCancelAdd` `Mathlib.Tactic.LinearCombination.smul_const_eq` `Mathlib.Tactic.LinearCombination.eq_rearrange` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.sub_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.zero_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.add_eq_eval₃` `Mathlib.Tactic.Module.NF.add_eq_eval₂` `zero_add` `Mathlib.Tactic.Module.NF.sub_eq_eval₂` `Mathlib.Tactic.Module.NF.zero_sub_eq_eval` `Mathlib.Tactic.Module.NF.eq_cons_const` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `mul_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.FieldSimp.subst_add` `neg_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `mul_neg` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `ne_of_gt` `norm_pos_iff` `Mathlib.Tactic.FieldSimp.zpow'_ofNat` `inner_smul_left` `conj_trivial` `instTrivialStarReal` `inner_self_eq_norm_sq_to_K` `mul_comm`
`hasEigenvector_of_isLocalExtrOn` 📖	mathematical	`IsSelfAdjoint` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.instStarId` `IsLocalExtrOn` `Real` `Real.instPreorder` `ContinuousLinearMap.reApplyInnerSelf` `Metric.sphere` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Norm.norm` `NormedAddCommGroup.toNorm`	`Module.End.HasEigenvector` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SeminormedAddCommGroup.toAddCommGroup` `ContinuousLinearMap.toLinearMap` `RCLike.ofReal` `ContinuousLinearMap.rayleighQuotient`	—	`Module.End.mem_eigenspace_iff` `eq_smul_self_of_isLocalExtrOn`
`hasEigenvector_of_isMaxOn` 📖	mathematical	`IsSelfAdjoint` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.instStarId` `IsMaxOn` `Real` `Real.instPreorder` `ContinuousLinearMap.reApplyInnerSelf` `Metric.sphere` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Norm.norm` `NormedAddCommGroup.toNorm`	`Module.End.HasEigenvector` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SeminormedAddCommGroup.toAddCommGroup` `ContinuousLinearMap.toLinearMap` `RCLike.ofReal` `iSup` `Real.instSupSet` `ContinuousLinearMap.rayleighQuotient`	—	`sub_zero` `ContinuousLinearMap.iSup_rayleigh_eq_iSup_rayleigh_sphere` `IsMaxOn.iSup_eq` `div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `le_of_lt` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `norm_pos_iff` `hasEigenvector_of_isLocalExtrOn` `IsMaxOn.localize`
`hasEigenvector_of_isMinOn` 📖	mathematical	`IsSelfAdjoint` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.instStarId` `IsMinOn` `Real` `Real.instPreorder` `ContinuousLinearMap.reApplyInnerSelf` `Metric.sphere` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Norm.norm` `NormedAddCommGroup.toNorm`	`Module.End.HasEigenvector` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SeminormedAddCommGroup.toAddCommGroup` `ContinuousLinearMap.toLinearMap` `RCLike.ofReal` `iInf` `Real.instInfSet` `ContinuousLinearMap.rayleighQuotient`	—	`sub_zero` `ContinuousLinearMap.iInf_rayleigh_eq_iInf_rayleigh_sphere` `IsMinOn.iInf_eq` `div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `le_of_lt` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `norm_pos_iff` `hasEigenvector_of_isLocalExtrOn` `IsMinOn.localize`
`linearly_dependent_of_isLocalExtrOn` 📖	mathematical	`IsSelfAdjoint` `ContinuousLinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `ContinuousLinearMap.instStarId` `IsLocalExtrOn` `Real.instPreorder` `ContinuousLinearMap.reApplyInnerSelf` `Metric.sphere` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Norm.norm` `NormedAddCommGroup.toNorm`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `DFunLike.coe` `ContinuousLinearMap.funLike`	—	`Set.ext` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `sub_zero` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `RingHomIsometric.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d` `hasStrictFDerivAt_norm_sq` `LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf` `isSymmetric` `LinearIsometry.injective` `LinearIsometry.map_add` `LinearIsometry.map_zero` `MulActionSemiHomClass.map_smulₛₗ` `SemilinearMapClass.toMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `LinearIsometry.instSemilinearIsometryClass` `smul_right_injective` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `Real.instIsDomain` `instIsTopologicalAddGroupReal` `GroupWithZero.toNoZeroSMulDivisors` `IsDomain.toIsCancelMulZero` `two_ne_zero` `CharZero.NeZero.two` `RCLike.charZero_rclike` `smul_add` `two_smul` `add_zero`

LinearMap.IsSymmetric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasEigenvalue_iInf_of_finiteDimensional` 📖	mathematical	`LinearMap.IsSymmetric` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Module.End.HasEigenvalue` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RCLike.ofReal` `iInf` `Real` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.instInfSet` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re` `Inner.inner` `InnerProductSpace.toInner` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `LinearMap.instFunLike` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`RingHomIsometric.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `complete_of_proper` `FiniteDimensional.proper_rclike` `exists_ne` `isCompact_sphere` `sub_zero` `IsCompact.exists_isMinOn` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Continuous.continuousOn` `ContinuousLinearMap.reApplyInnerSelf_continuous` `norm_norm` `Module.End.hasEigenvalue_of_hasEigenvector` `IsSelfAdjoint.hasEigenvector_of_isMinOn` `Subtype.prop`
`hasEigenvalue_iSup_of_finiteDimensional` 📖	mathematical	`LinearMap.IsSymmetric` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Module.End.HasEigenvalue` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RCLike.ofReal` `iSup` `Real` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real.instSupSet` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toZero` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Real.instAddMonoid` `AddMonoidHom.instFunLike` `RCLike.re` `Inner.inner` `InnerProductSpace.toInner` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `LinearMap.instFunLike` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`RingHomIsometric.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `complete_of_proper` `FiniteDimensional.proper_rclike` `exists_ne` `isCompact_sphere` `sub_zero` `IsCompact.exists_isMaxOn` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Continuous.continuousOn` `ContinuousLinearMap.reApplyInnerSelf_continuous` `norm_norm` `Module.End.hasEigenvalue_of_hasEigenvector` `IsSelfAdjoint.hasEigenvector_of_isMaxOn` `Subtype.prop`
`hasStrictFDerivAt_reApplyInnerSelf` 📖	mathematical	`LinearMap.IsSymmetric` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousLinearMap.toLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace`	`HasStrictFDerivAt` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `NormedAddCommGroup.toAddCommGroup` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Real.instAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `RCLike.innerProductSpace` `Real.pseudoMetricSpace` `ContinuousLinearMap.reApplyInnerSelf` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NontriviallyNormedField.toNormedField` `AddMonoid.toNatSMul` `ESeminormedAddMonoid.toAddMonoid` `ContinuousLinearMap.toNormedAddCommGroup` `Real.normedAddCommGroup` `RCLike.toInnerProductSpaceReal` `RingHomIsometric.ids` `Real.normedCommRing` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DFunLike.coe` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `starRingEnd` `RCLike.toStarRing` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.uniformContinuousConstSMul` `NormedRing.toRing` `NormedCommRing.toNormedRing` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ContinuousLinearMap.funLike` `innerSL`	—	`RingHomIsometric.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `RingHomCompTriple.ids` `ContinuousLinearMap.ext` `AddMonoid.continuousConstSMul_nat` `instIsTopologicalRingReal` `ContinuousLinearMap.smul_apply` `ContinuousLinearMap.comp_apply` `fderivInnerCLM_apply` `ContinuousLinearMap.prod_apply` `innerSL_apply_apply` `ContinuousLinearMap.id_apply` `apply_clm` `real_inner_comm` `Nat.instAtLeastTwoHAddOfNat` `two_smul` `HasStrictFDerivAt.inner` `ContinuousLinearMap.hasStrictFDerivAt` `hasStrictFDerivAt_id`
`subsingleton_of_no_eigenvalue_finiteDimensional` 📖	—	`LinearMap.IsSymmetric` `NormedAddCommGroup.toSeminormedAddCommGroup` `Module.End.eigenspace` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Bot.bot` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instBot`	—	—	`subsingleton_or_nontrivial` `hasEigenvalue_iSup_of_finiteDimensional`

---

← Back to Index