Documentation Verification Report

FiniteDimensional

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

Statistics

Metric	Count
Definitions `decomposition`	1
Theorems `reflections_generate`, `reflections_generate_dim`, `reflections_generate_dim_aux`, `isInternal_iff`, `isInternal_iff_of_isComplete`, `projection_directSum_coeAddHom`, `sum_projection_of_mem_iSup`, `det_reflection`, `finrank_add_finrank_orthogonal`, `finrank_add_finrank_orthogonal'`, `finrank_add_inf_finrank_orthogonal`, `finrank_add_inf_finrank_orthogonal'`, `finrank_orthogonal_span_singleton`, `linearEquiv_det_reflection`, `topologicalClosure_eq_self`, `maximal_orthonormal_iff_basis_of_finiteDimensional`, `maximal_orthonormal_iff_orthogonalComplement_eq_bot`	17
Total	18

LinearIsometryEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`reflections_generate` 📖	mathematical	—	`Subgroup.closure` `LinearIsometryEquiv` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Real.instRCLike` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `instGroup` `Set.range` `Submodule.reflection` `Submodule.orthogonal` `Submodule.span` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Set` `Set.instSingletonSet` `Submodule.instHasOrthogonalProjectionOrthogonal` `Submodule.HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Subtype.pseudoMetricSpace` `FiniteDimensional.RCLike.properSpace_submodule` `FiniteDimensional.span_singleton` `Real.instDivisionRing` `SeminormedAddCommGroup.toAddCommGroup` `Top.top` `Subgroup` `Subgroup.instTop`	—	`RingHomInvPair.ids` `Submodule.instHasOrthogonalProjectionOrthogonal` `Submodule.HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `FiniteDimensional.RCLike.properSpace_submodule` `FiniteDimensional.span_singleton` `Subgroup.eq_top_iff'` `reflections_generate_dim` `Subgroup.list_prod_mem` `Subgroup.subset_closure`
`reflections_generate_dim` 📖	mathematical	—	`Module.finrank` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Submodule.reflection` `Submodule.orthogonal` `Submodule.span` `Set` `Set.instSingletonSet` `Submodule.instHasOrthogonalProjectionOrthogonal` `Submodule.HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Subtype.pseudoMetricSpace` `FiniteDimensional.RCLike.properSpace_submodule` `FiniteDimensional.span_singleton` `Real.instDivisionRing` `SeminormedAddCommGroup.toAddCommGroup`	—	`RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Submodule.instHasOrthogonalProjectionOrthogonal` `Submodule.HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `FiniteDimensional.RCLike.properSpace_submodule` `FiniteDimensional.span_singleton` `reflections_generate_dim_aux` `le_rfl` `LE.le.trans` `Submodule.finrank_le` `commRing_strongRankCondition` `Real.instNontrivial`
`reflections_generate_dim_aux` 📖	mathematical	`Module.finrank` `Real` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Real.instRCLike` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `SetLike.instMembership` `Submodule.setLike` `Submodule.orthogonal` `LinearMap.ker` `Real.semiring` `Real.normedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.toLinearMap` `ContinuousLinearMap` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `ContinuousLinearMap.sub` `Real.instRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.id` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `toContinuousLinearEquiv` `Submodule.addCommMonoid` `Submodule.module`	`LinearIsometryEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `instGroup` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Submodule.reflection` `Submodule.span` `Set` `Set.instSingletonSet` `Submodule.instHasOrthogonalProjectionOrthogonal` `Submodule.HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `Subtype.pseudoMetricSpace` `FiniteDimensional.RCLike.properSpace_submodule` `FiniteDimensional.span_singleton` `Real.instDivisionRing`	—	`RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Submodule.instHasOrthogonalProjectionOrthogonal` `Submodule.HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `FiniteDimensional.RCLike.properSpace_submodule` `FiniteDimensional.span_singleton` `Eq.le` `Submodule.orthogonal_eq_bot_iff` `ContinuousLinearMap.completeSpace_ker` `FiniteDimensional.proper_real` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Submodule.finrank_eq_zero` `Real.instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `commRing_strongRankCondition` `Real.instNontrivial` `FiniteDimensional.finiteDimensional_submodule` `le_zero_iff` `ext` `LinearMap.congr_fun` `LinearMap.ker_eq_top` `sub_eq_zero` `LE.le.trans` `exists_ne` `Module.nontrivial_of_finrank_pos` `inner_map_map` `Subtype.prop` `Submodule.mem_left_iff_eq_zero_of_disjoint` `Submodule.orthogonal_disjoint` `RingHomCompTriple.ids` `Submodule.reflection_mem_subspace_eq_self` `Submodule.mem_orthogonal_singleton_iff_inner_left` `Submodule.sub_mem` `Submodule.reflection_sub` `norm_map` `Submodule.reflection_reflection` `Submodule.finrank_lt_finrank_of_lt` `SetLike.lt_iff_le_and_exists` `instIsConcreteLE` `Submodule.finrank_add_finrank_orthogonal` `one_mul` `Submodule.reflection_mul_reflection` `mul_assoc`

OrthogonalFamily

Definitions

Name	Category	Theorems
`decomposition` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isInternal_iff` 📖	mathematical	`OrthogonalFamily` `NormedAddCommGroup.toSeminormedAddCommGroup` `Submodule` `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` `SetLike.instMembership` `Submodule.setLike` `Submodule.seminormedAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule.innerProductSpace` `Submodule.subtypeₗᵢ`	`DirectSum.IsInternal` `Submodule.addSubmonoidClass` `Submodule.orthogonal` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Bot.bot` `Submodule.instBot`	—	`isInternal_iff_of_isComplete` `completeSpace_coe_iff_isComplete` `complete_of_proper` `FiniteDimensional.proper_rclike` `IsScalarTower.left` `FiniteDimensional.finiteDimensional_submodule`
`isInternal_iff_of_isComplete` 📖	mathematical	`OrthogonalFamily` `NormedAddCommGroup.toSeminormedAddCommGroup` `Submodule` `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` `SetLike.instMembership` `Submodule.setLike` `Submodule.seminormedAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule.innerProductSpace` `Submodule.subtypeₗᵢ` `IsComplete` `SetLike.coe` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice`	`DirectSum.IsInternal` `Submodule.addSubmonoidClass` `Submodule.orthogonal` `Bot.bot` `Submodule.instBot`	—	`Submodule.addSubmonoidClass` `independent` `Submodule.HasOrthogonalProjection.ofCompleteSpace` `IsComplete.completeSpace_coe`
`projection_directSum_coeAddHom` 📖	mathematical	`OrthogonalFamily` `NormedAddCommGroup.toSeminormedAddCommGroup` `Submodule` `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` `SetLike.instMembership` `Submodule.setLike` `Submodule.seminormedAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule.innerProductSpace` `Submodule.subtypeₗᵢ`	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceSubtype` `Submodule.addCommMonoid` `Submodule.module` `ContinuousLinearMap.funLike` `Submodule.orthogonalProjection` `Submodule.HasOrthogonalProjection.ofCompleteSpace` `AddMonoidHom` `DirectSum` `AddSubmonoidClass.toAddCommMonoid` `Submodule.addSubmonoidClass` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoidDirectSum` `AddMonoidHom.instFunLike` `DirectSum.coeAddMonoidHom` `DFinsupp` `AddZero.toZero` `DFinsupp.instDFunLike`	—	`DirectSum.induction_on` `Submodule.HasOrthogonalProjection.ofCompleteSpace` `Submodule.addSubmonoidClass` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `DirectSum.coeAddMonoidHom_of` `Decidable.eq_or_ne` `Submodule.orthogonalProjection_mem_subspace_eq_self` `DFinsupp.single_eq_same` `Submodule.orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero` `isOrtho` `Subtype.prop` `DFinsupp.single_eq_of_ne` `map_add` `AddMonoidHomClass.toAddHomClass` `SemilinearMapClass.toAddHomClass`
`sum_projection_of_mem_iSup` 📖	mathematical	`CompleteSpace` `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` `instUniformSpaceSubtype` `OrthogonalFamily` `Submodule.seminormedAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule.innerProductSpace` `Submodule.subtypeₗᵢ` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice`	`Finset.sum` `Finset.univ` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.funLike` `Submodule.starProjection` `Submodule.HasOrthogonalProjection.ofCompleteSpace`	—	`Submodule.iSup_induction'` `Submodule.HasOrthogonalProjection.ofCompleteSpace` `Finset.sum_eq_single_of_mem` `Finset.mem_univ` `Submodule.starProjection_apply` `Submodule.orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero` `isOrtho` `Submodule.coe_zero` `Submodule.starProjection_eq_self_iff` `Finset.sum_congr` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `Finset.sum_const_zero` `map_add` `SemilinearMapClass.toAddHomClass` `Finset.sum_add_distrib`

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`det_reflection` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring` `MonoidHom.instFunLike` `LinearMap.det` `LinearEquiv.toLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHomInvPair.ids` `LinearIsometryEquiv.toLinearEquiv` `reflection` `HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `Submodule` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SetLike.instMembership` `setLike` `Subtype.pseudoMetricSpace` `FiniteDimensional.RCLike.properSpace_submodule` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Module.finrank` `orthogonal` `addCommMonoid` `module`	—	`RingHomInvPair.ids` `HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `FiniteDimensional.RCLike.properSpace_submodule` `isCompl_orthogonal_of_hasOrthogonalProjection` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing` `smulCommClass_self` `Finite.instSum` `Finite.of_fintype` `RingHomCompTriple.ids` `Matrix.ext` `IsCompl.symm` `LinearMap.comp.congr_simp` `toLinearMap_prodEquivOfIsCompl_symm` `LinearMap.toMatrix_apply` `Module.Basis.prod_apply` `add_zero` `reflection_mem_subspace_eq_self` `linearProjOfIsCompl_apply_left` `linearProjOfIsCompl_apply_right` `Module.Basis.repr_self` `Finsupp.single_apply` `zero_add` `reflection_mem_subspace_orthogonalComplement_eq_neg` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `neg_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `LinearMap.det_conj` `LinearMap.det_toMatrix` `Matrix.det_fromBlocks_zero₂₁` `Matrix.det_one` `one_mul` `Matrix.det_neg` `Fintype.card_fin` `mul_one` `Module.finrank_of_infinite_dimensional` `pow_zero` `LinearMap.det_eq_one_of_finrank_eq_zero` `FiniteDimensional.finiteDimensional_submodule`
`finrank_add_finrank_orthogonal` 📖	mathematical	—	`Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `orthogonal`	—	`inf_top_eq` `finrank_top` `finrank_add_inf_finrank_orthogonal` `Module.Finite.top` `le_top`
`finrank_add_finrank_orthogonal'` 📖	mathematical	`Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `SetLike.instMembership` `setLike` `addCommMonoid` `module`	`orthogonal`	—	`AddLeftCancelSemigroup.toIsLeftCancelAdd` `finrank_add_finrank_orthogonal`
`finrank_add_inf_finrank_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` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Module.finrank` `SetLike.instMembership` `setLike` `addCommMonoid` `module` `instMin` `orthogonal`	—	`finrank_sup_add_finrank_inf_eq` `finiteDimensional_of_le` `finiteDimensional_inf_right` `add_zero` `sup_orthogonal_inf_of_hasOrthogonalProjection` `HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `FiniteDimensional.RCLike.properSpace_submodule` `finrank_bot` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `bot_inf_eq` `Disjoint.eq_bot` `orthogonal_disjoint` `inf_assoc`
`finrank_add_inf_finrank_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` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Module.finrank` `SetLike.instMembership` `setLike` `addCommMonoid` `module`	`instMin` `orthogonal`	—	`AddLeftCancelSemigroup.toIsLeftCancelAdd` `finrank_add_inf_finrank_orthogonal`
`finrank_orthogonal_span_singleton` 📖	mathematical	—	`Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `SetLike.instMembership` `setLike` `orthogonal` `span` `Set` `Set.instSingletonSet` `addCommMonoid` `module`	—	`finrank_add_finrank_orthogonal'` `FiniteDimensional.of_fact_finrank_eq_succ` `finrank_span_singleton` `add_comm` `Fact.elim`
`linearEquiv_det_reflection` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `LinearEquiv.automorphismGroup` `Units.instMulOneClass` `MonoidHom.instFunLike` `LinearEquiv.det` `LinearIsometryEquiv.toLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `reflection` `HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `Submodule` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SetLike.instMembership` `setLike` `Subtype.pseudoMetricSpace` `FiniteDimensional.RCLike.properSpace_submodule` `Monoid.toNatPow` `Units.instMonoid` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Units.instOne` `Module.finrank` `orthogonal` `addCommMonoid` `module`	—	`Units.ext` `RingHomInvPair.ids` `HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `FiniteDimensional.RCLike.properSpace_submodule` `LinearEquiv.coe_det` `Units.val_pow_eq_pow_val` `det_reflection`
`topologicalClosure_eq_self` 📖	mathematical	—	`topologicalClosure` `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` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	—	`IsClosed.submodule_topologicalClosure_eq` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `closed_of_finiteDimensional` `RCLike.toCompleteSpace` `IsBoundedSMul.continuousSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`maximal_orthonormal_iff_basis_of_finiteDimensional` 📖	mathematical	`Orthonormal` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instMembership`	`DFunLike.coe` `Module.Basis` `Set.Elem` `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` `Module.Basis.instFunLike`	—	`maximal_orthonormal_iff_orthogonalComplement_eq_bot` `Submodule.orthogonal_eq_bot_iff` `Submodule.HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `FiniteDimensional.RCLike.properSpace_submodule` `FiniteDimensional.finiteDimensional_submodule` `Subtype.range_coe_subtype` `Orthonormal.linearIndependent` `Eq.ge` `Module.Basis.span_eq`
`maximal_orthonormal_iff_orthogonalComplement_eq_bot` 📖	mathematical	`Orthonormal` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instMembership`	`Submodule.orthogonal` `Submodule.span` `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` `Bot.bot` `Submodule` `Submodule.instBot`	—	`Submodule.eq_bot_iff` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `norm_smul_inv_norm` `Submodule.smul_mem'` `Submodule.subset_span` `Submodule.inf_orthogonal_eq_bot` `Orthonormal.ne_zero` `Set.subset_insert` `Set.eq_or_mem_of_mem_insert` `inner_eq_zero_symm` `Set.ne_insert_of_notMem` `Not.imp_symm` `Finsupp.mem_span_image_iff_linearCombination` `Subtype.image_preimage_coe` `Set.inter_eq_self_of_subset_right` `Orthonormal.inner_finsupp_eq_zero`

---

← Back to Index