Basic

📁 Source: Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean

Statistics

Metric	Count
Definitions HasOrthogonalProjection, orthogonalProjection, orthogonalProjectionFn, starProjection	4
Theorems hasOrthogonalProjection_range, map_starProjection, map_starProjection', hasOrthogonalProjection_range, isSymmetricProjection_iff_eq_coe_starProjection, isSymmetricProjection_iff_eq_coe_starProjection_range, exists_orthogonal, map_linearIsometryEquiv, map_linearIsometryEquiv', ofCompleteSpace, orthogonalProjection_comp_subtypeL, starProjection_comp_starProjection, coe_orthogonalProjection_apply, eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero, eq_starProjection_of_mem_of_inner_eq_zero, eq_starProjection_of_mem_orthogonal, eq_starProjection_of_mem_orthogonal', exists_add_mem_mem_orthogonal, id_eq_sum_starProjection_self_orthogonalComplement, inner_orthogonalProjection_eq_of_mem_left, inner_orthogonalProjection_eq_of_mem_right, inner_starProjection_left_eq_right, instHasOrthogonalProjectionOfCompleteSpace, instHasOrthogonalProjectionOrthogonal, instHasOrthogonalProjectionTop, isIdempotentElem_starProjection, isSymmetricProjection_starProjection, ker_orthogonalProjection, ker_starProjection, lipschitzWith_orthogonalProjection, lipschitzWith_starProjection, mem_iff_norm_starProjection, norm_orthogonalProjection, norm_orthogonalProjection_apply, norm_orthogonalProjection_apply_le, norm_sq_eq_add_norm_sq_projection, norm_sq_eq_add_norm_sq_starProjection, norm_starProjection, norm_starProjection_apply, norm_starProjection_apply_le, orthogonalProjectionFn_eq, orthogonalProjectionFn_inner_eq_zero, orthogonalProjectionFn_mem, orthogonalProjectionFn_norm_sq, orthogonalProjection_bot, orthogonalProjection_comp_subtypeL_eq_zero_iff, orthogonalProjection_eq_zero_iff, orthogonalProjection_mem_subspace_eq_self, orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, orthogonalProjection_norm_le, orthogonalProjection_orthogonal, orthogonalProjection_orthogonalComplement_singleton_eq_zero, orthogonalProjection_orthogonal_apply_eq_zero, orthogonalProjection_starProjection_of_le, range_starProjection, re_inner_starProjection_eq_normSq, re_inner_starProjection_nonneg, smul_starProjection_singleton, starProjection_add_starProjection_orthogonal, starProjection_apply, starProjection_apply_eq_zero_iff, starProjection_apply_mem, starProjection_bot, starProjection_comp_starProjection_eq_zero_iff, starProjection_comp_starProjection_of_le, starProjection_eq_self_iff, starProjection_inner_eq_zero, starProjection_isSymmetric, starProjection_map_apply, starProjection_mem_subspace_eq_self, starProjection_minimal, starProjection_norm_le, starProjection_orthogonal, starProjection_orthogonal', starProjection_orthogonalComplement_singleton_eq_zero, starProjection_orthogonal_apply_eq_zero, starProjection_orthogonal_val, starProjection_singleton, starProjection_top, starProjection_top', starProjection_unit_singleton, sub_starProjection_mem_orthogonal	82
Total	86

ContinuousLinearMap.IsIdempotentElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasOrthogonalProjection_range 📖	mathematical	IsIdempotentElem 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.instMul	Submodule.HasOrthogonalProjection LinearMap.range RingHomSurjective.ids ContinuousLinearMap.toLinearMap	—	RingHomSurjective.ids IsClosed.completeSpace_coe isClosed_range SeminormedAddCommGroup.toIsTopologicalAddGroup T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Submodule.HasOrthogonalProjection.ofCompleteSpace

LinearIsometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_starProjection 📖	mathematical	—	DFunLike.coe LinearIsometry DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace instFunLike ContinuousLinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.funLike Submodule.starProjection Submodule.map AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup RingHomSurjective.ids toLinearMap	—	RingHomSurjective.ids Submodule.eq_starProjection_of_mem_of_inner_eq_zero Submodule.apply_coe_mem_map map_sub inner_map_map Submodule.starProjection_inner_eq_zero
map_starProjection' 📖	mathematical	—	DFunLike.coe LinearIsometry DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace instFunLike ContinuousLinearMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.funLike Submodule.starProjection Submodule.map RingHomSurjective.ids SemilinearMapClass.semilinearMap SemilinearIsometryClass.toSemilinearMapClass instSemilinearIsometryClass	—	RingHomSurjective.ids SemilinearIsometryClass.toSemilinearMapClass instSemilinearIsometryClass map_starProjection

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSymmetricProjection_iff_eq_coe_starProjection 📖	mathematical	—	IsSymmetricProjection NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule.starProjection	—	RingHomSurjective.ids isSymmetricProjection_iff_eq_coe_starProjection_range Submodule.isSymmetricProjection_starProjection
isSymmetricProjection_iff_eq_coe_starProjection_range 📖	mathematical	—	IsSymmetricProjection NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule.starProjection range RingHomSurjective.ids	—	RingHomSurjective.ids IsSymmetricProjection.hasOrthogonalProjection_range ext Submodule.eq_starProjection_of_mem_orthogonal IsIdempotentElem.isSymmetric_iff_orthogonal_range IsSymmetricProjection.isIdempotentElem IsSymmetricProjection.isSymmetric map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass IsIdempotentElem.mul_one_sub_self Submodule.isSymmetricProjection_starProjection

LinearMap.IsSymmetricProjection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasOrthogonalProjection_range 📖	mathematical	LinearMap.IsSymmetricProjection NormedAddCommGroup.toSeminormedAddCommGroup	Submodule.HasOrthogonalProjection LinearMap.range DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids	—	RingHomSurjective.ids LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range isIdempotentElem isSymmetric map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass IsIdempotentElem.eq sub_self

Submodule

Definitions

Name	Category	Theorems
HasOrthogonalProjection 📖	CompData	9 math math: EuclideanGeometry.orthogonalProjection_congr, HasOrthogonalProjection.ofCompleteSpace, instHasOrthogonalProjectionOfCompleteSpace, HasOrthogonalProjection.map_linearIsometryEquiv', LinearMap.IsSymmetricProjection.hasOrthogonalProjection_range, instHasOrthogonalProjectionOrthogonal, instHasOrthogonalProjectionTop, HasOrthogonalProjection.map_linearIsometryEquiv, ContinuousLinearMap.IsIdempotentElem.hasOrthogonalProjection_range
orthogonalProjection 📖	CompOp	53 math math: OrthonormalBasis.orthogonalProjection_eq_sum, re_inner_starProjection_eq_normSq, orthogonalProjection_mem_subspace_eq_self, OrthonormalBasis.orthogonalProjection_eq_sum_rankOne, EuclideanGeometry.orthogonalProjection_contLinear, LinearMap.IsSymmetric.directSum_decompose_apply, IsOrtho.orthogonalProjection_comp_subtypeL, orthogonalProjection_bot, EuclideanGeometry.orthogonalProjection_apply_mem, OrthonormalBasis.orthogonalProjection_apply_eq_sum, EuclideanGeometry.orthogonalProjection_apply', adjoint_subtypeL, orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, HilbertBasis.hasSum_orthogonalProjection, norm_orthogonalProjection_apply_le, stereoToFun_apply, coe_orthogonalDecomposition, norm_sq_eq_add_norm_sq_projection, starProjection_apply, fst_orthogonalDecomposition_apply, inner_orthogonalProjection_eq_of_mem_right, orthogonalProjection_apply_eq_linearProjOfIsCompl, sndL_comp_coe_orthogonalDecomposition, norm_orthogonalProjection_apply, inner_orthogonalProjection_eq_of_mem_left, toLinearMap_orthogonalProjection_eq_linearProjOfIsCompl, ker_orthogonalProjection, ContinuousLinearMap.IsPositive.orthogonalProjection_comp, dimH_orthogonalProjection_le, adjoint_orthogonalProjection, MeasureTheory.hausdorffMeasure_orthogonalProjection_le, lipschitzWith_orthogonalProjection, ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection, stereographic_apply, fstL_comp_coe_orthogonalDecomposition, EuclideanGeometry.orthogonalProjection_linear, orthogonalProjection_orthogonal_apply_eq_zero, orthogonalProjectionFn_eq, snd_orthogonalDecomposition_apply, orthogonalDecomposition_apply, EuclideanGeometry.orthogonalProjection_apply, norm_orthogonalProjection, EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection, orthogonalProjection_comp_subtypeL_eq_zero_iff, orthogonalProjection_eq_zero_iff, orthogonalProjection_starProjection_of_le, coe_orthogonalProjection_apply, orthogonalProjection_coe_eq_linearProjOfIsCompl, orthogonalProjection_norm_le, orthogonalProjection_orthogonal, orthogonalProjection_orthogonalComplement_singleton_eq_zero, orthogonalProjection_eq_linearProjOfIsCompl, OrthogonalFamily.projection_directSum_coeAddHom
orthogonalProjectionFn 📖	CompOp	5 math math: orthogonalProjectionFn_inner_eq_zero, orthogonalProjectionFn_eq, orthogonalProjectionFn_norm_sq, eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero, orthogonalProjectionFn_mem
starProjection 📖	CompOp	68 math math: starProjection_apply_eq_isComplProjection, IsOrtho.starProjection_comp_starProjection, re_inner_starProjection_eq_normSq, starProjection_orthogonal', starProjection_add_starProjection_orthogonal, starProjection_singleton, starProjection_comp_starProjection_eq_zero_iff, norm_starProjection_apply_le, LinearIsometry.map_starProjection', starProjection_tendsto_self, reflection_apply, InnerProductSpace.gramSchmidt_def, starProjection_inner_eq_zero, range_starProjection, starProjection_top', isIdempotentElem_starProjection, norm_sq_eq_add_norm_sq_starProjection, OrthonormalBasis.starProjection_eq_sum_rankOne, starProjection_inj, toLinearMap_starProjection_eq_isComplProjection, sub_starProjection_mem_orthogonal, starProjection_isSymmetric, starProjection_apply, smul_starProjection_singleton, starProjection_norm_le, norm_starProjection, eq_starProjection_of_mem_of_inner_eq_zero, starProjection_map_apply, starProjection_bot, starProjection_unit_singleton, isSelfAdjoint_starProjection, InnerProductSpace.gramSchmidt_def', isSymmetricProjection_starProjection, eq_starProjection_of_mem_orthogonal, LinearIsometry.map_starProjection, eq_starProjection_of_mem_orthogonal', starProjection_orthogonal, starProjection_apply_mem, isStarProjection_starProjection, ker_starProjection, starProjection_orthogonalComplement_singleton_eq_zero, starProjection_top, IsSelfAdjoint.conj_starProjection, lipschitzWith_starProjection, re_inner_starProjection_nonneg, OrthogonalFamily.sum_projection_of_mem_iSup, id_eq_sum_starProjection_self_orthogonalComplement, starProjection_orthogonal_apply_eq_zero, LinearMap.isSymmetricProjection_iff_eq_coe_starProjection, LinearMap.isSymmetricProjection_iff_eq_coe_starProjection_range, norm_starProjection_apply, inner_starProjection_left_eq_right, isStarProjection_iff_eq_starProjection_range, starProjection_minimal, starProjection_mem_subspace_eq_self, ContinuousLinearMap.IsPositive.conj_starProjection, starProjection_le_starProjection_iff, starProjection_orthogonal_val, isStarProjection_iff_eq_starProjection, starProjection_comp_starProjection_of_le, orthogonalProjection_starProjection_of_le, coe_orthogonalProjection_apply, starProjection_coe_eq_isCompl_projection, starProjection_apply_eq_zero_iff, orthogonalProjection_orthogonal, starProjection_eq_self_iff, starProjection_tendsto_closure_iSup, mem_iff_norm_starProjection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_orthogonalProjection_apply 📖	mathematical	—	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 setLike DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceSubtype addCommMonoid module ContinuousLinearMap.funLike orthogonalProjection starProjection	—	—
eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero 📖	mathematical	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 setLike Inner.inner InnerProductSpace.toInner SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing	orthogonalProjectionFn	—	sub_eq_zero inner_self_eq_zero sub_mem orthogonalProjectionFn_mem orthogonalProjectionFn_inner_eq_zero inner_sub_left sub_zero sub_sub_sub_cancel_left
eq_starProjection_of_mem_of_inner_eq_zero 📖	mathematical	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 setLike Inner.inner InnerProductSpace.toInner SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike starProjection	—	eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero
eq_starProjection_of_mem_orthogonal 📖	mathematical	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 setLike orthogonal SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike starProjection	—	eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero mem_orthogonal'
eq_starProjection_of_mem_orthogonal' 📖	mathematical	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 setLike orthogonal AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike starProjection	—	eq_starProjection_of_mem_orthogonal add_sub_cancel_left
exists_add_mem_mem_orthogonal 📖	mathematical	—	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 setLike orthogonal AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	Subtype.coe_prop sub_starProjection_mem_orthogonal add_sub_cancel
id_eq_sum_starProjection_self_orthogonalComplement 📖	mathematical	—	ContinuousLinearMap.id DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.add IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup starProjection orthogonal instHasOrthogonalProjectionOrthogonal	—	ContinuousLinearMap.ext IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup instHasOrthogonalProjectionOrthogonal starProjection_add_starProjection_orthogonal
inner_orthogonalProjection_eq_of_mem_left 📖	mathematical	—	Inner.inner 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 setLike InnerProductSpace.toInner seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing innerProductSpace DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceSubtype addCommMonoid module ContinuousLinearMap.funLike orthogonalProjection	—	inner_conj_symm inner_orthogonalProjection_eq_of_mem_right
inner_orthogonalProjection_eq_of_mem_right 📖	mathematical	—	Inner.inner 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 setLike InnerProductSpace.toInner seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing innerProductSpace DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceSubtype addCommMonoid module ContinuousLinearMap.funLike orthogonalProjection	—	coe_inner starProjection_inner_eq_zero coe_mem add_zero inner_add_left add_sub_cancel
inner_starProjection_left_eq_right 📖	mathematical	—	Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace ContinuousLinearMap.funLike starProjection	—	inner_orthogonalProjection_eq_of_mem_right
instHasOrthogonalProjectionOfCompleteSpace 📖	mathematical	—	HasOrthogonalProjection ClosedSubmodule.toSubmodule 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	—	HasOrthogonalProjection.ofCompleteSpace instCompleteSpaceSubtypeMemSubmoduleOfIsClosedCoe ClosedSubmodule.isClosed'
instHasOrthogonalProjectionOrthogonal 📖	mathematical	—	HasOrthogonalProjection orthogonal	—	HasOrthogonalProjection.exists_orthogonal sub_sub_cancel le_orthogonal_orthogonal
instHasOrthogonalProjectionTop 📖	mathematical	—	HasOrthogonalProjection Top.top 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 instTop	—	top_orthogonal_eq_bot sub_self AddSubmonoidClass.toZeroMemClass addSubmonoidClass
isIdempotentElem_starProjection 📖	mathematical	—	IsIdempotentElem 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.instMul starProjection	—	ContinuousLinearMap.ext starProjection_eq_self_iff
isSymmetricProjection_starProjection 📖	mathematical	—	LinearMap.IsSymmetricProjection NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace starProjection	—	ContinuousLinearMap.IsIdempotentElem.toLinearMap isIdempotentElem_starProjection starProjection_isSymmetric
ker_orthogonalProjection 📖	mathematical	—	LinearMap.ker 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 setLike addCommMonoid module RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.toLinearMap instTopologicalSpaceSubtype orthogonalProjection orthogonal	—	ext orthogonalProjection_eq_zero_iff
ker_starProjection 📖	mathematical	—	LinearMap.ker 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 ContinuousLinearMap.toLinearMap starProjection orthogonal	—	RingHomSurjective.ids LinearMap.IsIdempotentElem.ker_eq_range ContinuousLinearMap.IsIdempotentElem.toLinearMap isIdempotentElem_starProjection instHasOrthogonalProjectionOrthogonal range_starProjection SeminormedAddCommGroup.toIsTopologicalAddGroup starProjection_orthogonal ContinuousLinearMap.coe_sub ContinuousLinearMap.coe_id
lipschitzWith_orthogonalProjection 📖	mathematical	—	LipschitzWith 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 setLike EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace instPseudoEMetricSpaceSubtype NNReal instOneNNReal DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceSubtype addCommMonoid module ContinuousLinearMap.funLike orthogonalProjection	—	ContinuousLinearMap.lipschitzWith_of_opNorm_le IsScalarTower.left RingHomIsometric.ids orthogonalProjection_norm_le
lipschitzWith_starProjection 📖	mathematical	—	LipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace NNReal instOneNNReal DFunLike.coe 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.funLike starProjection	—	ContinuousLinearMap.lipschitzWith_of_opNorm_le RingHomIsometric.ids starProjection_norm_le
mem_iff_norm_starProjection 📖	mathematical	—	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 setLike Norm.norm NormedAddCommGroup.toNorm DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike starProjection	—	norm_starProjection_apply instHasOrthogonalProjectionOrthogonal starProjection_orthogonal_val AddLeftCancelSemigroup.toIsLeftCancelAdd isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat norm_sq_eq_add_norm_sq_starProjection
norm_orthogonalProjection 📖	mathematical	—	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 Submodule NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership setLike instTopologicalSpaceSubtype addCommMonoid module ContinuousLinearMap.hasOpNorm seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNontriviallyNormedField normedSpace Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id NontriviallyNormedField.toNormedField IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction orthogonalProjection Real Real.instOne	—	le_antisymm IsScalarTower.left orthogonalProjection_norm_le exists_mem_ne_zero_of_ne_bot norm_orthogonalProjection_apply div_self ContinuousLinearMap.ratio_le_opNorm RingHomIsometric.ids
norm_orthogonalProjection_apply 📖	mathematical	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 setLike	Norm.norm NormedAddCommGroup.toNorm normedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceSubtype addCommMonoid module ContinuousLinearMap.funLike orthogonalProjection	—	starProjection_eq_self_iff
norm_orthogonalProjection_apply_le 📖	mathematical	—	Real Real.instLE Norm.norm 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 setLike NormedAddCommGroup.toNorm normedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceSubtype addCommMonoid module ContinuousLinearMap.funLike orthogonalProjection	—	IsScalarTower.left ContinuousLinearMap.le_opNorm RingHomIsometric.ids mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing orthogonalProjection_norm_le norm_nonneg one_mul
norm_sq_eq_add_norm_sq_projection 📖	mathematical	—	Real Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm Real.instAdd 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 setLike normedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceSubtype addCommMonoid module ContinuousLinearMap.funLike orthogonalProjection orthogonal instHasOrthogonalProjectionOrthogonal	—	instHasOrthogonalProjectionOrthogonal starProjection_add_starProjection_orthogonal sq norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero mem_orthogonal
norm_sq_eq_add_norm_sq_starProjection 📖	mathematical	—	Real Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm Real.instAdd DFunLike.coe 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.funLike starProjection orthogonal instHasOrthogonalProjectionOrthogonal	—	norm_sq_eq_add_norm_sq_projection
norm_starProjection 📖	mathematical	—	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 ContinuousLinearMap.hasOpNorm DenselyNormedField.toNontriviallyNormedField starProjection Real Real.instOne	—	norm_orthogonalProjection
norm_starProjection_apply 📖	mathematical	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 setLike	Norm.norm NormedAddCommGroup.toNorm DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike starProjection	—	norm_orthogonalProjection_apply
norm_starProjection_apply_le 📖	mathematical	—	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm DFunLike.coe 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.funLike starProjection	—	norm_orthogonalProjection_apply_le
orthogonalProjectionFn_eq 📖	mathematical	—	orthogonalProjectionFn 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 setLike DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceSubtype addCommMonoid module ContinuousLinearMap.funLike orthogonalProjection	—	—
orthogonalProjectionFn_inner_eq_zero 📖	mathematical	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 setLike	Inner.inner InnerProductSpace.toInner SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup orthogonalProjectionFn MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing	—	mem_orthogonal' HasOrthogonalProjection.exists_orthogonal
orthogonalProjectionFn_mem 📖	mathematical	—	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 setLike orthogonalProjectionFn	—	HasOrthogonalProjection.exists_orthogonal
orthogonalProjectionFn_norm_sq 📖	mathematical	—	Real Real.instMul Norm.norm NormedAddCommGroup.toNorm Real.instAdd SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup orthogonalProjectionFn	—	orthogonalProjectionFn_inner_eq_zero orthogonalProjectionFn_mem sub_add_cancel norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero
orthogonalProjection_bot 📖	mathematical	—	orthogonalProjection Bot.bot 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 instBot HasOrthogonalProjection.ofCompleteSpace complete_of_proper SetLike.instMembership setLike Subtype.pseudoMetricSpace FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_bot NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceSubtype addCommMonoid module ContinuousLinearMap.zero	—	ContinuousLinearMap.ext HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_bot bot_ext
orthogonalProjection_comp_subtypeL_eq_zero_iff 📖	mathematical	—	ContinuousLinearMap.comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring Submodule ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership setLike instTopologicalSpaceSubtype addCommMonoid module RingHomCompTriple.ids orthogonalProjection subtypeL ContinuousLinearMap ContinuousLinearMap.zero IsOrtho	—	RingHomCompTriple.ids DFunLike.congr_fun starProjection_apply coe_zero sub_zero starProjection_inner_eq_zero IsOrtho.orthogonalProjection_comp_subtypeL
orthogonalProjection_eq_zero_iff 📖	mathematical	—	DFunLike.coe 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 Submodule NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership setLike instTopologicalSpaceSubtype addCommMonoid module ContinuousLinearMap.funLike orthogonalProjection zero orthogonal	—	sub_zero coe_zero sub_starProjection_mem_orthogonal eq_starProjection_of_mem_orthogonal ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass addSubmonoidClass
orthogonalProjection_mem_subspace_eq_self 📖	mathematical	—	DFunLike.coe 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 Submodule NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership setLike instTopologicalSpaceSubtype addCommMonoid module ContinuousLinearMap.funLike orthogonalProjection	—	eq_starProjection_of_mem_of_inner_eq_zero sub_self inner_zero_left
orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero 📖	mathematical	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 setLike orthogonal	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceSubtype addCommMonoid module ContinuousLinearMap.funLike orthogonalProjection zero	—	orthogonalProjection_eq_zero_iff
orthogonalProjection_norm_le 📖	mathematical	—	Real Real.instLE 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 Submodule NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership setLike instTopologicalSpaceSubtype addCommMonoid module ContinuousLinearMap.hasOpNorm seminormedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNontriviallyNormedField normedSpace Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id NontriviallyNormedField.toNormedField IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction orthogonalProjection Real.instOne	—	LinearMap.mkContinuous_norm_le IsScalarTower.left orthogonalProjectionFn_mem Real.instZeroLEOneClass
orthogonalProjection_orthogonal 📖	mathematical	—	DFunLike.coe 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 Submodule NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership setLike orthogonal instTopologicalSpaceSubtype addCommMonoid module ContinuousLinearMap.funLike orthogonalProjection instHasOrthogonalProjectionOrthogonal SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup starProjection sub_starProjection_mem_orthogonal	—	instHasOrthogonalProjectionOrthogonal sub_starProjection_mem_orthogonal starProjection_orthogonal_val
orthogonalProjection_orthogonalComplement_singleton_eq_zero 📖	mathematical	—	DFunLike.coe 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 Submodule NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership setLike orthogonal span Set Set.instSingletonSet instTopologicalSpaceSubtype addCommMonoid module ContinuousLinearMap.funLike orthogonalProjection instHasOrthogonalProjectionOrthogonal HasOrthogonalProjection.ofCompleteSpace complete_of_proper Subtype.pseudoMetricSpace FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing SeminormedAddCommGroup.toAddCommGroup zero	—	orthogonalProjection_orthogonal_apply_eq_zero instHasOrthogonalProjectionOrthogonal HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton mem_span_singleton_self
orthogonalProjection_orthogonal_apply_eq_zero 📖	mathematical	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 setLike	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring orthogonal instTopologicalSpaceSubtype addCommMonoid module ContinuousLinearMap.funLike orthogonalProjection zero	—	orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero le_orthogonal_orthogonal
orthogonalProjection_starProjection_of_le 📖	mathematical	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 Preorder.toLE PartialOrder.toPreorder instPartialOrder	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring SetLike.instMembership setLike instTopologicalSpaceSubtype addCommMonoid module ContinuousLinearMap.funLike orthogonalProjection starProjection	—	map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero orthogonal_le sub_starProjection_mem_orthogonal
range_starProjection 📖	mathematical	—	LinearMap.range 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 RingHomSurjective.ids ContinuousLinearMap.toLinearMap starProjection	—	ext RingHomSurjective.ids coe_mem starProjection_eq_self_iff
re_inner_starProjection_eq_normSq 📖	mathematical	—	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace ContinuousLinearMap.funLike starProjection Monoid.toNatPow Real.instMonoid Norm.norm Submodule SetLike.instMembership setLike NormedAddCommGroup.toNorm normedAddCommGroup NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing instTopologicalSpaceSubtype addCommMonoid module orthogonalProjection	—	starProjection_apply Nat.instAtLeastTwoHAddOfNat re_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two div_eq_iff CharZero.NeZero.two RCLike.charZero_rclike pow_two add_sub_assoc eq_sub_iff_add_eq' coe_norm mul_sub_one Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_one mul_one sub_eq_iff_eq_add' norm_sub_rev orthogonalProjectionFn_norm_sq
re_inner_starProjection_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero DFunLike.coe AddMonoidHom AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace ContinuousLinearMap.funLike starProjection	—	re_inner_starProjection_eq_normSq sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
smul_starProjection_singleton 📖	mathematical	—	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 RCLike.ofReal Real Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike starProjection span Set Set.instSingletonSet HasOrthogonalProjection.ofCompleteSpace complete_of_proper Submodule SetLike.instMembership setLike Subtype.pseudoMetricSpace FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing SeminormedAddCommGroup.toAddCommGroup Inner.inner InnerProductSpace.toInner	—	HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton eq_starProjection_of_mem_of_inner_eq_zero mem_span_singleton mem_orthogonal' mem_orthogonal_singleton_iff_inner_left inner_sub_left inner_smul_left map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RCLike.conj_ofReal mul_comm inner_conj_symm inner_self_eq_norm_sq_to_K sub_self map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
starProjection_add_starProjection_orthogonal 📖	mathematical	—	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring NormedSpace.toModule InnerProductSpace.toNormedSpace ContinuousLinearMap.funLike starProjection orthogonal instHasOrthogonalProjectionOrthogonal	—	instHasOrthogonalProjectionOrthogonal starProjection_orthogonal_val add_sub_cancel
starProjection_apply 📖	mathematical	—	DFunLike.coe 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.funLike starProjection Submodule SetLike.instMembership setLike instTopologicalSpaceSubtype addCommMonoid module orthogonalProjection	—	—
starProjection_apply_eq_zero_iff 📖	mathematical	—	DFunLike.coe 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.funLike starProjection NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Submodule SetLike.instMembership setLike orthogonal	—	starProjection_eq_self_iff inner_starProjection_left_eq_right inner_zero_right orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero
starProjection_apply_mem 📖	mathematical	—	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 setLike DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike starProjection	—	—
starProjection_bot 📖	mathematical	—	starProjection Bot.bot 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 instBot HasOrthogonalProjection.ofCompleteSpace complete_of_proper SetLike.instMembership setLike Subtype.pseudoMetricSpace FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_bot NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing SeminormedAddCommGroup.toAddCommGroup ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.zero	—	HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule finiteDimensional_bot starProjection.eq_1 orthogonalProjection_bot ContinuousLinearMap.comp_zero
starProjection_comp_starProjection_eq_zero_iff 📖	mathematical	—	ContinuousLinearMap.comp 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 RingHomCompTriple.ids starProjection ContinuousLinearMap ContinuousLinearMap.zero IsOrtho	—	RingHomCompTriple.ids orthogonalProjection_comp_subtypeL_eq_zero_iff orthogonalProjection_mem_subspace_eq_self IsOrtho.starProjection_comp_starProjection
starProjection_comp_starProjection_of_le 📖	mathematical	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 Preorder.toLE PartialOrder.toPreorder instPartialOrder	ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids starProjection	—	ContinuousLinearMap.ext RingHomCompTriple.ids starProjection.eq_1 orthogonalProjection_starProjection_of_le
starProjection_eq_self_iff 📖	mathematical	—	DFunLike.coe 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.funLike starProjection Submodule SetLike.instMembership setLike	—	eq_starProjection_of_mem_of_inner_eq_zero sub_self inner_zero_left
starProjection_inner_eq_zero 📖	mathematical	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 setLike	Inner.inner InnerProductSpace.toInner SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike starProjection MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing	—	orthogonalProjectionFn_inner_eq_zero
starProjection_isSymmetric 📖	mathematical	—	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace starProjection	—	inner_starProjection_left_eq_right
starProjection_map_apply 📖	mathematical	—	DFunLike.coe 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.funLike starProjection map AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup RingHomSurjective.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearIsometryEquiv.toLinearEquiv HasOrthogonalProjection.map_linearIsometryEquiv LinearIsometryEquiv EquivLike.toFunLike LinearIsometryEquiv.instEquivLike LinearIsometryEquiv.symm	—	RingHomInvPair.ids RingHomSurjective.ids SemilinearIsometryClass.toSemilinearMapClass LinearIsometry.instSemilinearIsometryClass HasOrthogonalProjection.map_linearIsometryEquiv' LinearIsometryEquiv.apply_symm_apply LinearIsometry.map_starProjection'
starProjection_mem_subspace_eq_self 📖	mathematical	—	DFunLike.coe 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.funLike starProjection Submodule SetLike.instMembership setLike	—	orthogonalProjection_mem_subspace_eq_self
starProjection_minimal 📖	mathematical	—	Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup DFunLike.coe 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.funLike starProjection iInf Real Submodule SetLike.instMembership setLike Real.instInfSet	—	starProjection_apply norm_eq_iInf_iff_inner_eq_zero coe_mem starProjection_inner_eq_zero
starProjection_norm_le 📖	mathematical	—	Real Real.instLE 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 ContinuousLinearMap.hasOpNorm DenselyNormedField.toNontriviallyNormedField starProjection Real.instOne	—	orthogonalProjection_norm_le
starProjection_orthogonal 📖	mathematical	—	starProjection orthogonal instHasOrthogonalProjectionOrthogonal 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.sub NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.id	—	ContinuousLinearMap.ext instHasOrthogonalProjectionOrthogonal SeminormedAddCommGroup.toIsTopologicalAddGroup sub_starProjection_mem_orthogonal orthogonalProjection_orthogonal
starProjection_orthogonal' 📖	mathematical	—	starProjection orthogonal instHasOrthogonalProjectionOrthogonal 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.sub NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.one	—	starProjection_orthogonal
starProjection_orthogonalComplement_singleton_eq_zero 📖	mathematical	—	DFunLike.coe 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.funLike starProjection orthogonal span Set Set.instSingletonSet instHasOrthogonalProjectionOrthogonal HasOrthogonalProjection.ofCompleteSpace complete_of_proper Submodule SetLike.instMembership setLike Subtype.pseudoMetricSpace FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing SeminormedAddCommGroup.toAddCommGroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	instHasOrthogonalProjectionOrthogonal HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton starProjection_apply coe_eq_zero orthogonalProjection_orthogonalComplement_singleton_eq_zero
starProjection_orthogonal_apply_eq_zero 📖	mathematical	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 setLike	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike starProjection orthogonal NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	starProjection_apply coe_eq_zero orthogonalProjection_orthogonal_apply_eq_zero
starProjection_orthogonal_val 📖	mathematical	—	DFunLike.coe 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.funLike starProjection orthogonal instHasOrthogonalProjectionOrthogonal SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	eq_starProjection_of_mem_orthogonal' instHasOrthogonalProjectionOrthogonal sub_starProjection_mem_orthogonal le_orthogonal_orthogonal sub_add_cancel
starProjection_singleton 📖	mathematical	—	DFunLike.coe 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.funLike starProjection span Set Set.instSingletonSet HasOrthogonalProjection.ofCompleteSpace complete_of_proper Submodule SetLike.instMembership setLike Subtype.pseudoMetricSpace FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing SeminormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Inner.inner InnerProductSpace.toInner RCLike.ofReal Real Monoid.toNatPow Real.instMonoid Norm.norm NormedAddCommGroup.toNorm	—	HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton span_zero_singleton starProjection.congr_simp starProjection_bot inner_zero_left norm_zero zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass div_zero smul_zero ne_of_gt norm_pos_iff SemigroupAction.mul_smul smul_starProjection_singleton Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast Nat.cast_one algebraMap.coe_pow Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul 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.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero IsLocalRing.toNontrivial Field.instIsLocalRing one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval 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 Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero
starProjection_top 📖	mathematical	—	starProjection Top.top 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 instTop instHasOrthogonalProjectionTop ContinuousLinearMap.id	—	ContinuousLinearMap.ext instHasOrthogonalProjectionTop starProjection_eq_self_iff
starProjection_top' 📖	mathematical	—	starProjection Top.top 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 instTop instHasOrthogonalProjectionTop ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.one	—	starProjection_top
starProjection_unit_singleton 📖	mathematical	Norm.norm NormedAddCommGroup.toNorm Real Real.instOne	DFunLike.coe 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.funLike starProjection span Set Set.instSingletonSet HasOrthogonalProjection.ofCompleteSpace complete_of_proper Submodule SetLike.instMembership setLike Subtype.pseudoMetricSpace FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing SeminormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Inner.inner InnerProductSpace.toInner	—	HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton smul_starProjection_singleton one_pow map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass one_smul
sub_starProjection_mem_orthogonal 📖	mathematical	—	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 setLike orthogonal SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike starProjection	—	inner_eq_zero_symm starProjection_inner_eq_zero

Submodule.HasOrthogonalProjection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_orthogonal 📖	mathematical	—	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 Submodule.orthogonal SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	—
map_linearIsometryEquiv 📖	mathematical	—	Submodule.HasOrthogonalProjection Submodule.map DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearIsometryEquiv.toLinearEquiv	—	RingHomInvPair.ids RingHomSurjective.ids exists_orthogonal Submodule.mem_map_of_mem Set.forall_mem_image LinearIsometryEquiv.inner_map_map LinearIsometryEquiv.symm_apply_apply map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearIsometryClass.toSemilinearMapClass SemilinearIsometryEquivClass.toSemilinearIsometryClass LinearIsometryEquiv.instSemilinearIsometryEquivClass
map_linearIsometryEquiv' 📖	mathematical	—	Submodule.HasOrthogonalProjection Submodule.map 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 RingHomSurjective.ids SemilinearMapClass.semilinearMap LinearIsometry LinearIsometryEquiv.toLinearIsometry RingHomInvPair.ids LinearIsometry.instFunLike SemilinearIsometryClass.toSemilinearMapClass LinearIsometry.instSemilinearIsometryClass	—	RingHomInvPair.ids map_linearIsometryEquiv
ofCompleteSpace 📖	mathematical	—	Submodule.HasOrthogonalProjection	—	Submodule.exists_norm_eq_iInf_of_complete_subspace completeSpace_coe_iff_isComplete Submodule.mem_orthogonal' Submodule.norm_eq_iInf_iff_inner_eq_zero

Submodule.IsOrtho

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
orthogonalProjection_comp_subtypeL 📖	mathematical	Submodule.IsOrtho	ContinuousLinearMap.comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring Submodule ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module RingHomCompTriple.ids Submodule.orthogonalProjection Submodule.subtypeL ContinuousLinearMap ContinuousLinearMap.zero	—	ContinuousLinearMap.ext RingHomCompTriple.ids Submodule.orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero symm Subtype.prop
starProjection_comp_starProjection 📖	mathematical	Submodule.IsOrtho	ContinuousLinearMap.comp 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 RingHomCompTriple.ids Submodule.starProjection ContinuousLinearMap ContinuousLinearMap.zero	—	RingHomCompTriple.ids ContinuousLinearMap.comp.congr_simp orthogonalProjection_comp_subtypeL ContinuousLinearMap.zero_comp ContinuousLinearMap.comp_zero

---

← Back to Index