PiL2

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

Statistics

Metric	Count
Definitions `isometryOfOrthonormal`, `orthonormalBasisOneI`, `collectedOrthonormalBasis`, `isometryL2OfOrthogonalFamily`, `sigmaOrthonormalBasisIndexEquiv`, `subordinateOrthonormalBasis`, `subordinateOrthonormalBasisIndex`, `basisFun`, `delabVecNotation`, `equiv`, `finAddEquivProd`, `proj`, `projₗ`, `restrict₂`, `single`, `sumEquivProd`, `extend`, `toEuclideanLin`, `toOrthonormalBasis`, `OrthonormalBasis`, `equiv`, `fromOrthogonalSpanSingleton`, `instFunLike`, `instInhabited`, `map`, `mk`, `mkOfOrthogonalEqBot`, `reindex`, `repr`, `singleton`, `span`, `toBasis`, `orthonormalBasis`, `innerProductSpace`, `vecNotation`, `stdOrthonormalBasis`	36
Theorems `coe_orthonormalBasisOneI`, `isometryOfOrthonormal_apply`, `isometryOfOrthonormal_symm_apply`, `map_isometryOfOrthonormal`, `orthonormalBasisOneI_repr_apply`, `orthonormalBasisOneI_repr_symm_apply`, `toBasis_orthonormalBasisOneI`, `card_filter_subordinateOrthonormalBasisIndex_eq`, `collectedOrthonormalBasis_mem`, `exists_subordinateOrthonormalBasisIndex_eq`, `isometryL2OfOrthogonalFamily_symm_apply`, `sigmaOrthonormalBasisIndexEquiv_def`, `subordinateOrthonormalBasisIndex_def`, `subordinateOrthonormalBasis_def`, `subordinateOrthonormalBasis_subordinate`, `ball_zero_eq`, `basisFun_apply`, `basisFun_inner`, `basisFun_repr`, `basisFun_toBasis`, `closedBall_zero_eq`, `coe_proj`, `dist_eq`, `dist_single_same`, `dist_sq_eq`, `edist_eq`, `edist_single_same`, `infinite`, `inner_basisFun_real`, `inner_eq_star_dotProduct`, `inner_single_left`, `inner_single_right`, `inner_toLp_toLp`, `instFactEqNatFinrankFin`, `nndist_eq`, `nndist_single_same`, `nnnorm_eq`, `nnnorm_single`, `norm_eq`, `norm_single`, `norm_sq_eq`, `ofLp_single`, `orthonormal_single`, `piLpCongrLeft_single`, `real_norm_sq_eq`, `restrict₂_apply`, `single_apply`, `single_eq_zero_iff`, `sphere_zero_eq`, `toLp_single`, `symm_toEuclideanLin_rankOne`, `toMatrix_rankOne`, `extend_apply`, `toMatrix_innerₛₗ_apply`, `ofLp_toEuclideanLin_apply`, `piLp_ofLp_toEuclideanLin`, `toEuclideanLin_apply`, `toEuclideanLin_apply_piLp_toLp`, `toEuclideanLin_eq_toLin`, `toEuclideanLin_eq_toLin_orthonormal`, `toEuclideanLin_toLp`, `coe_toOrthonormalBasis`, `coe_toOrthonormalBasis_repr`, `coe_toOrthonormalBasis_repr_symm`, `toBasis_toOrthonormalBasis`, `exists_orthonormalBasis_extension`, `exists_orthonormalBasis_extension_of_card_eq`, `coe_equiv_euclideanSpace`, `coe_mk`, `coe_ofRepr`, `coe_of_orthogonal_eq_bot_mk`, `coe_reindex`, `coe_singleton`, `coe_toBasis`, `coe_toBasis_repr`, `coe_toBasis_repr_apply`, `det_to_matrix_orthonormalBasis`, `det_to_matrix_orthonormalBasis_real`, `enorm_eq_one`, `equiv_apply`, `equiv_apply_basis`, `equiv_apply_euclideanSpace`, `equiv_self_rfl`, `equiv_symm`, `inner_eq_ite`, `inner_eq_one`, `inner_eq_zero`, `map_apply`, `nnnorm_eq_one`, `norm_eq_one`, `norm_le_card_mul_iSup_norm_inner`, `orthogonalProjection_apply_eq_sum`, `orthogonalProjection_eq_sum`, `orthogonalProjection_eq_sum_rankOne`, `orthonormal`, `reindex_apply`, `reindex_toBasis`, `repr_apply_apply`, `repr_injective`, `repr_reindex`, `repr_self`, `repr_symm_single`, `singleton_apply`, `singleton_repr`, `span_apply`, `starProjection_eq_sum_rankOne`, `sum_inner_mul_inner`, `sum_rankOne_eq_id`, `sum_repr`, `sum_repr'`, `sum_repr_symm`, `sum_sq_inner_left`, `sum_sq_inner_right`, `sum_sq_norm_inner_left`, `sum_sq_norm_inner_right`, `toBasis_map`, `toBasis_singleton`, `toMatrix_orthonormalBasis_conjTranspose_mul_self`, `toMatrix_orthonormalBasis_mem_orthogonal`, `toMatrix_orthonormalBasis_mem_unitary`, `toMatrix_orthonormalBasis_self_mul_conjTranspose`, `toBasis`, `orthonormalBasis_apply`, `orthonormalBasis_repr`, `inner_apply`, `exists_orthonormalBasis`, `finrank_euclideanSpace`, `finrank_euclideanSpace_fin`, `inner_matrix_col_col`, `inner_matrix_row_row`, `orthonormalBasis_one_dim`, `stdOrthonormalBasis_def`, `toMatrix_innerSL_apply`	133
Total	169

Complex

Definitions

Name	Category	Theorems
`isometryOfOrthonormal` 📖	CompOp	3 math math: `isometryOfOrthonormal_apply`, `isometryOfOrthonormal_symm_apply`, `map_isometryOfOrthonormal`
`orthonormalBasisOneI` 📖	CompOp	4 math math: `toBasis_orthonormalBasisOneI`, `coe_orthonormalBasisOneI`, `orthonormalBasisOneI_repr_apply`, `orthonormalBasisOneI_repr_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_orthonormalBasisOneI` 📖	mathematical	—	`DFunLike.coe` `OrthonormalBasis` `Real` `Real.instRCLike` `Complex` `instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `Fin.fintype` `OrthonormalBasis.instFunLike` `orthonormalBasisOneI` `Matrix.vecCons` `instOne` `I` `Matrix.vecEmpty`	—	`Module.Basis.coe_toOrthonormalBasis` `coe_basisOneI`
`isometryOfOrthonormal_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Complex` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceRealComplex` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `isometryOfOrthonormal` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `re` `OrthonormalBasis` `Fin.fintype` `OrthonormalBasis.instFunLike` `im`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `OrthonormalBasis.sum_repr_symm` `Finset.sum_congr` `Fin.sum_univ_two` `Matrix.cons_val_fin_one`
`isometryOfOrthonormal_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Complex` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceRealComplex` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `isometryOfOrthonormal` `instAdd` `ofReal` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `LinearMap.instFunLike` `Module.Basis.coord` `OrthonormalBasis.toBasis` `Fin.fintype` `instMul` `I`	—	`fact_one_le_two_ennreal` `RingHomInvPair.ids` `OrthonormalBasis.coe_toBasis_repr_apply`
`map_isometryOfOrthonormal` 📖	mathematical	—	`isometryOfOrthonormal` `OrthonormalBasis.map` `Real` `Real.instRCLike` `Fin.fintype` `LinearIsometryEquiv.trans` `Complex` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `RingHomCompTriple.ids` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `InnerProductSpace.toNormedSpace` `instInnerProductSpaceRealComplex`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `fact_one_le_two_ennreal` `LinearIsometryEquiv.trans_assoc`
`orthonormalBasisOneI_repr_apply` 📖	mathematical	—	`WithLp.ofLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `DFunLike.coe` `LinearIsometryEquiv` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Real.instRCLike` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Complex` `EuclideanSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instNormedAddCommGroup` `PiLp.seminormedAddCommGroup` `fact_one_le_two_ennreal` `Fin.fintype` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `instInnerProductSpaceRealComplex` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `RCLike.innerProductSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `OrthonormalBasis.repr` `orthonormalBasisOneI` `Matrix.vecCons` `re` `im` `Matrix.vecEmpty`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal`
`orthonormalBasisOneI_repr_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Real.instRCLike` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EuclideanSpace` `Complex` `PiLp.seminormedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Fin.fintype` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedAddCommGroup.toSeminormedAddCommGroup` `instNormedAddCommGroup` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `instInnerProductSpaceRealComplex` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `OrthonormalBasis.repr` `orthonormalBasisOneI` `instAdd` `ofReal` `WithLp.ofLp` `instMul` `I`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal`
`toBasis_orthonormalBasisOneI` 📖	mathematical	—	`OrthonormalBasis.toBasis` `Real` `Real.instRCLike` `Complex` `instNormedAddCommGroup` `instInnerProductSpaceRealComplex` `Fin.fintype` `orthonormalBasisOneI` `basisOneI`	—	`Module.Basis.toBasis_toOrthonormalBasis`

DirectSum.IsInternal

Definitions

Name	Category	Theorems
`collectedOrthonormalBasis` 📖	CompOp	2 math math: `subordinateOrthonormalBasis_def`, `collectedOrthonormalBasis_mem`
`isometryL2OfOrthogonalFamily` 📖	CompOp	1 math math: `isometryL2OfOrthogonalFamily_symm_apply`
`sigmaOrthonormalBasisIndexEquiv` 📖	CompOp	3 math math: `sigmaOrthonormalBasisIndexEquiv_def`, `subordinateOrthonormalBasis_def`, `subordinateOrthonormalBasisIndex_def`
`subordinateOrthonormalBasis` 📖	CompOp	3 math math: `subordinateOrthonormalBasis_subordinate`, `subordinateOrthonormalBasis_def`, `LinearMap.IsSymmetric.eigenvectorBasis_def`
`subordinateOrthonormalBasisIndex` 📖	CompOp	4 math math: `exists_subordinateOrthonormalBasisIndex_eq`, `subordinateOrthonormalBasis_subordinate`, `card_filter_subordinateOrthonormalBasisIndex_eq`, `subordinateOrthonormalBasisIndex_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_filter_subordinateOrthonormalBasisIndex_eq` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `DirectSum.IsInternal` `Submodule` `Submodule.setLike` `Submodule.addSubmonoidClass` `OrthogonalFamily` `SetLike.instMembership` `Submodule.seminormedAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule.innerProductSpace` `Submodule.subtypeₗᵢ`	`Finset.card` `Finset.filter` `subordinateOrthonormalBasisIndex` `Finset.univ` `Fin.fintype` `Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	`Submodule.addSubmonoidClass` `Finset.card_eq_of_equiv_fin`
`collectedOrthonormalBasis_mem` 📖	mathematical	`DirectSum.IsInternal` `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` `Submodule.setLike` `Submodule.addSubmonoidClass` `OrthogonalFamily` `SetLike.instMembership` `Submodule.seminormedAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule.innerProductSpace` `Submodule.subtypeₗᵢ`	`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` `DFunLike.coe` `OrthonormalBasis` `Sigma.instFintype` `OrthonormalBasis.instFunLike` `collectedOrthonormalBasis`	—	`Submodule.addSubmonoidClass` `Module.Basis.coe_toOrthonormalBasis` `collectedBasis_coe`
`exists_subordinateOrthonormalBasisIndex_eq` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `DirectSum.IsInternal` `Submodule` `Submodule.setLike` `Submodule.addSubmonoidClass` `OrthogonalFamily` `SetLike.instMembership` `Submodule.seminormedAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule.innerProductSpace` `Submodule.subtypeₗᵢ`	`subordinateOrthonormalBasisIndex`	—	`Submodule.addSubmonoidClass` `subordinateOrthonormalBasisIndex_def` `Equiv.symm_apply_apply`
`isometryL2OfOrthogonalFamily_symm_apply` 📖	mathematical	`DirectSum.IsInternal` `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` `Submodule.setLike` `Submodule.addSubmonoidClass` `OrthogonalFamily` `SetLike.instMembership` `Submodule.seminormedAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule.innerProductSpace` `Submodule.subtypeₗᵢ`	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `PiLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `Submodule` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `SetLike.instMembership` `Submodule.setLike` `PiLp.seminormedAddCommGroup` `fact_one_le_two_ennreal` `Submodule.seminormedAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.module` `Submodule.addCommMonoid` `Submodule.module` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `isometryL2OfOrthogonalFamily` `Finset.sum` `Finset.univ` `WithLp.ofLp`	—	`Submodule.addSubmonoidClass` `Nat.instAtLeastTwoHAddOfNat` `RingHomInvPair.ids` `DFinsupp.sumAddHom_apply` `DFinsupp.sum_eq_sum_fintype` `Finset.sum_congr`
`sigmaOrthonormalBasisIndexEquiv_def` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `DirectSum.IsInternal` `Submodule` `Submodule.setLike` `OrthogonalFamily` `SetLike.instMembership` `Submodule.seminormedAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule.innerProductSpace` `Submodule.subtypeₗᵢ`	`sigmaOrthonormalBasisIndexEquiv`	—	`Submodule.addSubmonoidClass`
`subordinateOrthonormalBasisIndex_def` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `DirectSum.IsInternal` `Submodule` `Submodule.setLike` `OrthogonalFamily` `SetLike.instMembership` `Submodule.seminormedAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule.innerProductSpace` `Submodule.subtypeₗᵢ`	`subordinateOrthonormalBasisIndex` `Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `sigmaOrthonormalBasisIndexEquiv`	—	`Submodule.addSubmonoidClass`
`subordinateOrthonormalBasis_def` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `DirectSum.IsInternal` `Submodule` `Submodule.setLike` `OrthogonalFamily` `SetLike.instMembership` `Submodule.seminormedAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule.innerProductSpace` `Submodule.subtypeₗᵢ`	`subordinateOrthonormalBasis` `OrthonormalBasis.reindex` `Module.finrank` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `SetLike.instMembership` `Submodule.setLike` `Submodule.normedAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule.innerProductSpace` `Sigma.instFintype` `Fin.fintype` `collectedOrthonormalBasis` `stdOrthonormalBasis` `sigmaOrthonormalBasisIndexEquiv`	—	`Submodule.addSubmonoidClass`
`subordinateOrthonormalBasis_subordinate` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `DirectSum.IsInternal` `Submodule` `Submodule.setLike` `Submodule.addSubmonoidClass` `OrthogonalFamily` `SetLike.instMembership` `Submodule.seminormedAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule.innerProductSpace` `Submodule.subtypeₗᵢ`	`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` `subordinateOrthonormalBasisIndex` `DFunLike.coe` `OrthonormalBasis` `Fin.fintype` `OrthonormalBasis.instFunLike` `subordinateOrthonormalBasis`	—	`Submodule.addSubmonoidClass` `subordinateOrthonormalBasisIndex_def` `subordinateOrthonormalBasis_def` `OrthonormalBasis.coe_reindex` `collectedOrthonormalBasis_mem` `FiniteDimensional.finiteDimensional_submodule`

EuclideanSpace

Definitions

Name	Category	Theorems
`basisFun` 📖	CompOp	11 math math: `basisFun_toBasis`, `basisFun_apply`, `ProbabilityTheory.covarianceBilin_apply_basisFun_self`, `basisFun_repr`, `OrthonormalBasis.equiv_apply_euclideanSpace`, `ProbabilityTheory.covarianceBilin_apply_basisFun`, `Matrix.IsHermitian.eigenvectorUnitary_coe`, `basisFun_inner`, `inner_basisFun_real`, `OrthonormalBasis.coe_equiv_euclideanSpace`, `Matrix.toEuclideanLin_eq_toLin_orthonormal`
`delabVecNotation` 📖	CompOp	—
`equiv` 📖	CompOp	4 math math: `Pi.comul_eq_adjoint`, `Matrix.l2_opNorm_mulVec`, `Pi.counit_eq_adjoint`, `Matrix.l2_opNNNorm_mulVec`
`finAddEquivProd` 📖	CompOp	—
`proj` 📖	CompOp	1 math math: `coe_proj`
`projₗ` 📖	CompOp	—
`restrict₂` 📖	CompOp	2 math math: `ProbabilityTheory.measurePreserving_restrict₂_multivariateGaussian`, `restrict₂_apply`
`single` 📖	CompOp	17 math math: `orthonormal_single`, `inner_single_left`, `basisFun_apply`, `OrthonormalBasis.repr_self`, `norm_single`, `dist_single_same`, `OrthonormalBasis.coe_ofRepr`, `nnnorm_single`, `edist_single_same`, `toLp_single`, `piLpCongrLeft_single`, `ofLp_single`, `OrthonormalBasis.repr_symm_single`, `inner_single_right`, `single_eq_zero_iff`, `nndist_single_same`, `single_apply`
`sumEquivProd` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ball_zero_eq` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Metric.ball` `EuclideanSpace` `Real` `PiLp.instPseudoMetricSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Real.pseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `Real.instAddCommGroup` `setOf` `Real.instLT` `Finset.sum` `Real.instAddCommMonoid` `Finset.univ` `Monoid.toPow` `Real.instMonoid` `WithLp.ofLp`	—	`Set.ext` `fact_one_le_two_ennreal` `Finset.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `sq_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Finset.sum_congr` `norm_eq` `sq_abs` `Real.sqrt_lt`
`basisFun_apply` 📖	mathematical	—	`DFunLike.coe` `OrthonormalBasis` `EuclideanSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `PiLp.innerProductSpace` `RCLike.innerProductSpace` `OrthonormalBasis.instFunLike` `basisFun` `single` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`PiLp.basisFun_apply` `Finite.of_fintype`
`basisFun_inner` 📖	mathematical	—	`Inner.inner` `EuclideanSpace` `InnerProductSpace.toInner` `PiLp.seminormedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `PiLp.innerProductSpace` `RCLike.innerProductSpace` `DFunLike.coe` `OrthonormalBasis` `PiLp.normedAddCommGroup` `OrthonormalBasis.instFunLike` `basisFun` `WithLp.ofLp`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal`
`basisFun_repr` 📖	mathematical	—	`WithLp.ofLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EuclideanSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `PiLp.seminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `PiLp.innerProductSpace` `RCLike.innerProductSpace` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `OrthonormalBasis.repr` `basisFun`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal`
`basisFun_toBasis` 📖	mathematical	—	`OrthonormalBasis.toBasis` `EuclideanSpace` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `PiLp.innerProductSpace` `RCLike.innerProductSpace` `basisFun` `PiLp.basisFun` `Finite.of_fintype` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`fact_one_le_two_ennreal`
`closedBall_zero_eq` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Metric.closedBall` `EuclideanSpace` `Real` `PiLp.instPseudoMetricSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Real.pseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `Real.instAddCommGroup` `setOf` `Real.instLE` `Finset.sum` `Real.instAddCommMonoid` `Finset.univ` `Monoid.toPow` `Real.instMonoid` `WithLp.ofLp`	—	`Set.ext` `fact_one_le_two_ennreal` `Finset.sum_congr` `norm_eq` `sq_abs` `Real.sqrt_le_left`
`coe_proj` 📖	mathematical	—	`DFunLike.coe` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `EuclideanSpace` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `WithLp.instModule` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `proj` `WithLp.ofLp`	—	—
`dist_eq` 📖	mathematical	—	`Dist.dist` `EuclideanSpace` `PiLp.instDist` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Real.sqrt` `Finset.sum` `Real` `Real.instAddCommMonoid` `Finset.univ` `Monoid.toPow` `Real.instMonoid` `WithLp.ofLp`	—	`PiLp.dist_eq_of_L2`
`dist_single_same` 📖	mathematical	—	`Dist.dist` `EuclideanSpace` `PiLp.instDist` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `single`	—	`PiLp.dist_single_same` `fact_one_le_two_ennreal`
`dist_sq_eq` 📖	mathematical	—	`Real` `Monoid.toPow` `Real.instMonoid` `Dist.dist` `EuclideanSpace` `PiLp.instDist` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `PseudoMetricSpace.toDist` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Finset.sum` `Real.instAddCommMonoid` `Finset.univ` `WithLp.ofLp`	—	`PiLp.dist_sq_eq_of_L2`
`edist_eq` 📖	mathematical	—	`EDist.edist` `EuclideanSpace` `PiLp.instEDist` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `PseudoEMetricSpace.toEDist` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedField.toMetricSpace` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Real` `ENNReal.instPowReal` `Finset.sum` `ENNReal.instAddCommMonoid` `Finset.univ` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `WithLp.ofLp` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`PiLp.edist_eq_of_L2`
`edist_single_same` 📖	mathematical	—	`EDist.edist` `EuclideanSpace` `PiLp.instEDist` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `PseudoEMetricSpace.toEDist` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedField.toMetricSpace` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `single`	—	`PiLp.edist_single_same` `fact_one_le_two_ennreal`
`infinite` 📖	mathematical	—	`Infinite` `EuclideanSpace`	—	`Module.Free.infinite` `Module.Free.of_divisionRing` `NontriviallyNormedField.infinite` `WithLp.instNontrivial` `Function.nontrivial` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`inner_basisFun_real` 📖	mathematical	—	`Inner.inner` `Real` `EuclideanSpace` `InnerProductSpace.toInner` `Real.instRCLike` `PiLp.seminormedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `NormedAddCommGroup.toSeminormedAddCommGroup` `Real.normedAddCommGroup` `PiLp.innerProductSpace` `RCLike.toInnerProductSpaceReal` `DFunLike.coe` `OrthonormalBasis` `PiLp.normedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.innerProductSpace` `OrthonormalBasis.instFunLike` `basisFun` `WithLp.ofLp`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `real_inner_comm` `basisFun_inner`
`inner_eq_star_dotProduct` 📖	mathematical	—	`Inner.inner` `EuclideanSpace` `InnerProductSpace.toInner` `PiLp.seminormedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `PiLp.innerProductSpace` `RCLike.innerProductSpace` `dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `WithLp.ofLp` `Star.star` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `RCLike.toStarRing`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal`
`inner_single_left` 📖	mathematical	—	`Inner.inner` `EuclideanSpace` `InnerProductSpace.toInner` `PiLp.seminormedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `PiLp.innerProductSpace` `RCLike.innerProductSpace` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.instFunLike` `starRingEnd` `RCLike.toStarRing` `WithLp.ofLp`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `Finset.sum_congr` `PiLp.single_apply` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `mul_ite` `mul_comm` `MulZeroClass.zero_mul` `Finset.sum_ite_eq'`
`inner_single_right` 📖	mathematical	—	`Inner.inner` `EuclideanSpace` `InnerProductSpace.toInner` `PiLp.seminormedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `PiLp.innerProductSpace` `RCLike.innerProductSpace` `single` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.instFunLike` `starRingEnd` `RCLike.toStarRing` `WithLp.ofLp`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `Finset.sum_congr` `PiLp.single_apply` `ite_mul` `MulZeroClass.zero_mul` `Finset.sum_ite_eq'`
`inner_toLp_toLp` 📖	mathematical	—	`Inner.inner` `WithLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `InnerProductSpace.toInner` `PiLp.seminormedAddCommGroup` `fact_one_le_two_ennreal` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `PiLp.innerProductSpace` `RCLike.innerProductSpace` `WithLp.toLp` `dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Star.star` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `RCLike.toStarRing`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal`
`instFactEqNatFinrankFin` 📖	mathematical	—	`Fact` `Module.finrank` `EuclideanSpace` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `Fin.fintype` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace`	—	`fact_one_le_two_ennreal` `finrank_euclideanSpace_fin`
`nndist_eq` 📖	mathematical	—	`NNDist.nndist` `EuclideanSpace` `PseudoMetricSpace.toNNDist` `PiLp.instPseudoMetricSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `DFunLike.coe` `OrderIso` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `NNReal.instPartialOrder` `instFunLikeOrderIso` `NNReal.sqrt` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NNReal.instSemiring` `Finset.univ` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `WithLp.ofLp`	—	`PiLp.nndist_eq_of_L2`
`nndist_single_same` 📖	mathematical	—	`NNDist.nndist` `EuclideanSpace` `PseudoMetricSpace.toNNDist` `PiLp.instPseudoMetricSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `single`	—	`fact_one_le_two_ennreal` `PiLp.nndist_single_same`
`nnnorm_eq` 📖	mathematical	—	`NNNorm.nnnorm` `EuclideanSpace` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `PiLp.seminormedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `DFunLike.coe` `OrderIso` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `NNReal.instPartialOrder` `instFunLikeOrderIso` `NNReal.sqrt` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NNReal.instSemiring` `Finset.univ` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `WithLp.ofLp`	—	`PiLp.nnnorm_eq_of_L2`
`nnnorm_single` 📖	mathematical	—	`NNNorm.nnnorm` `EuclideanSpace` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `PiLp.seminormedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `single`	—	`fact_one_le_two_ennreal` `PiLp.nnnorm_single`
`norm_eq` 📖	mathematical	—	`Norm.norm` `EuclideanSpace` `PiLp.instNorm` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Real.sqrt` `Finset.sum` `Real` `Real.instAddCommMonoid` `Finset.univ` `Monoid.toPow` `Real.instMonoid` `WithLp.ofLp`	—	`Finset.sum_congr` `fact_one_le_two_ennreal` `Real.coe_sqrt` `NNReal.coe_sum` `nnnorm_eq`
`norm_single` 📖	mathematical	—	`Norm.norm` `EuclideanSpace` `PiLp.instNorm` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `single`	—	`PiLp.norm_single` `fact_one_le_two_ennreal`
`norm_sq_eq` 📖	mathematical	—	`Real` `Monoid.toPow` `Real.instMonoid` `Norm.norm` `EuclideanSpace` `PiLp.instNorm` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Finset.sum` `Real.instAddCommMonoid` `Finset.univ` `WithLp.ofLp`	—	`PiLp.norm_sq_eq_of_L2`
`ofLp_single` 📖	mathematical	—	`WithLp.ofLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `single` `Pi.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField`	—	—
`orthonormal_single` 📖	mathematical	—	`Orthonormal` `EuclideanSpace` `PiLp.seminormedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `PiLp.innerProductSpace` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `RCLike.innerProductSpace` `single` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`fact_one_le_two_ennreal` `inner_single_left` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_mul` `PiLp.single_apply`
`piLpCongrLeft_single` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `PiLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `PiLp.seminormedAddCommGroup` `fact_one_le_two_ennreal` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `AddCommGroup.toAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.piLpCongrLeft` `single` `Equiv` `Equiv.instEquivLike`	—	`LinearIsometryEquiv.piLpCongrLeft_single` `Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal`
`real_norm_sq_eq` 📖	mathematical	—	`Real` `Monoid.toPow` `Real.instMonoid` `Norm.norm` `EuclideanSpace` `PiLp.instNorm` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Real.norm` `Finset.sum` `Real.instAddCommMonoid` `Finset.univ` `WithLp.ofLp`	—	`norm_sq_eq` `Finset.sum_congr` `sq_abs`
`restrict₂_apply` 📖	mathematical	`Finset` `Finset.instHasSubset`	`WithLp.ofLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `EuclideanSpace` `Finset` `SetLike.instMembership` `Finset.instSetLike` `PiLp.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `Finset.Subtype.fintype` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `ContinuousLinearMap.funLike` `restrict₂`	—	`fact_one_le_two_ennreal`
`single_apply` 📖	mathematical	—	`WithLp.ofLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField`	—	`PiLp.single_apply`
`single_eq_zero_iff` 📖	mathematical	—	`single` `EuclideanSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `WithLp.instAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Pi.addCommGroup` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	—
`sphere_zero_eq` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Metric.sphere` `EuclideanSpace` `Real` `PiLp.instPseudoMetricSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `Real.pseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `Real.instAddCommGroup` `setOf` `Finset.sum` `Real.instAddCommMonoid` `Finset.univ` `Monoid.toPow` `Real.instMonoid` `WithLp.ofLp`	—	`Set.ext` `fact_one_le_two_ennreal` `Finset.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `sq_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Finset.sum_congr` `norm_eq` `sq_abs` `Real.sqrt_eq_iff_eq_sq`
`toLp_single` 📖	mathematical	—	`WithLp.toLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Pi.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `single`	—	—

InnerProductSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`symm_toEuclideanLin_rankOne` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `EuclideanSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `NormedAddCommGroup.toAddCommGroup` `WithLp.instModule` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `toNormedSpace` `RCLike.innerProductSpace` `Matrix` `LinearMap.addCommMonoid` `Matrix.addCommMonoid` `LinearMap.module` `WithLp.instSMulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `Function.smulCommClass` `AddCommMonoid.toAddMonoid` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Matrix.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `Matrix.toEuclideanLin` `ContinuousLinearMap.toLinearMap` `SeminormedAddCommGroup.toPseudoMetricSpace` `PiLp.seminormedAddCommGroup` `PiLp.innerProductSpace` `PiLp.normedSpace` `ContinuousLinearMap` `starRingEnd` `RCLike.toStarRing` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `CommMonoid.toMonoid` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.funLike` `ContinuousLinearMap.addCommGroup` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `DenselyNormedField.toNontriviallyNormedField` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `ContinuousLinearMap.continuousConstSMul` `rankOne` `Matrix.vecMulVec` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `WithLp.ofLp` `Star.star` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `WithLp.instSMulCommClass` `Function.smulCommClass` `Algebra.to_smulCommClass` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.topologicalAddGroup` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `ContinuousLinearMap.continuousConstSMul` `Nat.instAtLeastTwoHAddOfNat` `EuclideanSpace.inner_single_right` `one_mul` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `mul_comm` `Matrix.ext_iff`
`toMatrix_rankOne` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `toNormedSpace` `Matrix` `LinearMap.addCommMonoid` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Matrix.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearMap.toMatrix` `OrthonormalBasis.toBasis` `ContinuousLinearMap.toLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `ContinuousLinearMap` `starRingEnd` `RCLike.toStarRing` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousLinearMap.module` `CommRing.toCommMonoid` `Field.toCommRing` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `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` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.funLike` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `DenselyNormedField.toNontriviallyNormedField` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `ContinuousLinearMap.continuousConstSMul` `rankOne` `Matrix.vecMulVec` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Finsupp` `Finsupp.instFunLike` `Finsupp.instAddCommMonoid` `Finsupp.module` `Module.Basis.repr` `Star.star` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid` `WithLp.ofLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `LinearIsometryEquiv` `EuclideanSpace` `PiLp.seminormedAddCommGroup` `fact_one_le_two_ennreal` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `WithLp.instModule` `Pi.addCommGroup` `Pi.Function.module` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `SeminormedRing.toRing` `RCLike.innerProductSpace` `LinearIsometryEquiv.instEquivLike` `OrthonormalBasis.repr`	—	`RingHomInvPair.ids` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.topologicalAddGroup` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `ContinuousLinearMap.continuousConstSMul` `fact_one_le_two_ennreal` `RingHomCompTriple.ids` `IsBoundedSMul.continuousSMul` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `rankOne_def'` `ContinuousLinearMap.coe_comp` `ContinuousLinearMap.toLinearMap_toSpanSingleton` `Finite.of_fintype` `LinearMap.toMatrix_comp` `LinearMap.toMatrix_toSpanSingleton` `ContinuousLinearMap.toLinearMap_innerSL_apply` `LinearMap.toMatrix_innerₛₗ_apply` `OrthonormalBasis.toBasis_singleton` `Module.Basis.coe_singleton` `Matrix.vecMulVec_one` `OrthonormalBasis.coe_singleton` `star_one` `Matrix.one_vecMulVec` `Matrix.vecMulVec_eq`

LinearIsometry

Definitions

Name	Category	Theorems
`extend` 📖	CompOp	1 math math: `extend_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extend_apply` 📖	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` `extend` `Submodule` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.seminormedAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule.module`	—	`fact_one_le_two_ennreal` `Submodule.orthogonalProjection_mem_subspace_eq_self` `Submodule.orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero` `Submodule.orthogonal_orthogonal` `Submodule.HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `FiniteDimensional.RCLike.properSpace_submodule` `FiniteDimensional.finiteDimensional_submodule` `AddLeftCancelSemigroup.toIsLeftCancelAdd`

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toMatrix_innerₛₗ_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `Matrix` `addCommMonoid` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Matrix.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toMatrix` `Finite.of_fintype` `OrthonormalBasis.toBasis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `starRingEnd` `RCLike.toStarRing` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `Algebra.to_smulCommClass` `Algebra.id` `instFunLike` `innerₛₗ` `Matrix.vecMulVec` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `Star.star` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid` `OrthonormalBasis` `OrthonormalBasis.instFunLike` `WithLp.ofLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `LinearIsometryEquiv` `EuclideanSpace` `PiLp.seminormedAddCommGroup` `fact_one_le_two_ennreal` `WithLp.instModule` `Pi.addCommGroup` `Pi.Function.module` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `LinearIsometryEquiv.instEquivLike` `OrthonormalBasis.repr`	—	`Matrix.ext` `RingHomInvPair.ids` `smulCommClass_self` `Finite.of_fintype` `Algebra.to_smulCommClass` `fact_one_le_two_ennreal` `toMatrix_apply` `OrthonormalBasis.coe_toBasis_repr_apply` `OrthonormalBasis.repr_apply_apply` `mul_comm` `inner_conj_symm`

Matrix

Definitions

Name	Category	Theorems
`toEuclideanLin` 📖	CompOp	16 math math: `spectrum_toEuclideanLin`, `toEuclideanLin_apply`, `piLp_ofLp_toEuclideanLin`, `isSymmetric_toEuclideanLin_iff`, `isPositive_toEuclideanLin_iff`, `l2_opNNNorm_def`, `coe_toEuclideanCLM_eq_toEuclideanLin`, `toEuclideanLin_eq_toLin`, `isHermitian_iff_isSymmetric`, `toEuclideanLin_conjTranspose_eq_adjoint`, `ofLp_toEuclideanLin_apply`, `toEuclideanLin_apply_piLp_toLp`, `toEuclideanLin_eq_toLin_orthonormal`, `l2_opNorm_def`, `toEuclideanLin_toLp`, `InnerProductSpace.symm_toEuclideanLin_rankOne`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofLp_toEuclideanLin_apply` 📖	mathematical	—	`WithLp.ofLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `EuclideanSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `PiLp.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `NormedAddCommGroup.toAddCommGroup` `WithLp.instModule` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `LinearMap.instFunLike` `LinearEquiv` `RingHomInvPair.ids` `Matrix` `addCommMonoid` `LinearMap.addCommMonoid` `module` `LinearMap.module` `WithLp.instSMulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `Function.smulCommClass` `AddCommMonoid.toAddMonoid` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toEuclideanLin` `mulVec` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`fact_one_le_two_ennreal` `RingHomInvPair.ids` `WithLp.instSMulCommClass` `Function.smulCommClass` `Algebra.to_smulCommClass`
`piLp_ofLp_toEuclideanLin` 📖	mathematical	—	`WithLp.ofLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `EuclideanSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `PiLp.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `NormedAddCommGroup.toAddCommGroup` `WithLp.instModule` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `LinearMap.instFunLike` `LinearEquiv` `RingHomInvPair.ids` `Matrix` `addCommMonoid` `LinearMap.addCommMonoid` `module` `LinearMap.module` `WithLp.instSMulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `Function.smulCommClass` `AddCommMonoid.toAddMonoid` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toEuclideanLin` `Pi.addCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `toLin'`	—	`fact_one_le_two_ennreal` `RingHomInvPair.ids` `WithLp.instSMulCommClass` `Function.smulCommClass` `Algebra.to_smulCommClass`
`toEuclideanLin_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `EuclideanSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `NormedAddCommGroup.toAddCommGroup` `WithLp.instModule` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `LinearMap.instFunLike` `LinearEquiv` `RingHomInvPair.ids` `Matrix` `addCommMonoid` `LinearMap.addCommMonoid` `module` `LinearMap.module` `WithLp.instSMulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `Function.smulCommClass` `AddCommMonoid.toAddMonoid` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toEuclideanLin` `WithLp.toLp` `mulVec` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `WithLp.ofLp`	—	`fact_one_le_two_ennreal` `RingHomInvPair.ids` `WithLp.instSMulCommClass` `Function.smulCommClass` `Algebra.to_smulCommClass`
`toEuclideanLin_apply_piLp_toLp` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `EuclideanSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `NormedAddCommGroup.toAddCommGroup` `WithLp.instModule` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `LinearMap.instFunLike` `LinearEquiv` `RingHomInvPair.ids` `Matrix` `addCommMonoid` `LinearMap.addCommMonoid` `module` `LinearMap.module` `WithLp.instSMulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `Function.smulCommClass` `AddCommMonoid.toAddMonoid` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toEuclideanLin` `WithLp.toLp` `mulVec` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`fact_one_le_two_ennreal` `RingHomInvPair.ids` `WithLp.instSMulCommClass` `Function.smulCommClass` `Algebra.to_smulCommClass`
`toEuclideanLin_eq_toLin` 📖	mathematical	—	`toEuclideanLin` `toLin` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `EuclideanSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `NormedAddCommGroup.toAddCommGroup` `WithLp.instModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `PiLp.basisFun` `Finite.of_fintype`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `WithLp.instSMulCommClass` `Function.smulCommClass` `Algebra.to_smulCommClass`
`toEuclideanLin_eq_toLin_orthonormal` 📖	mathematical	—	`toEuclideanLin` `toLin` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Finite.of_fintype` `EuclideanSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `PiLp.innerProductSpace` `RCLike.innerProductSpace` `OrthonormalBasis.toBasis` `EuclideanSpace.basisFun`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `WithLp.instSMulCommClass` `Function.smulCommClass` `Algebra.to_smulCommClass`
`toEuclideanLin_toLp` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `EuclideanSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `NormedAddCommGroup.toAddCommGroup` `WithLp.instModule` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `LinearMap.instFunLike` `LinearEquiv` `RingHomInvPair.ids` `Matrix` `addCommMonoid` `LinearMap.addCommMonoid` `module` `LinearMap.module` `WithLp.instSMulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Module.toDistribMulAction` `Function.smulCommClass` `AddCommMonoid.toAddMonoid` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toEuclideanLin` `WithLp.toLp` `Pi.addCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `toLin'`	—	`fact_one_le_two_ennreal` `RingHomInvPair.ids` `WithLp.instSMulCommClass` `Function.smulCommClass` `Algebra.to_smulCommClass`

Module.Basis

Definitions

Name	Category	Theorems
`toOrthonormalBasis` 📖	CompOp	4 math math: `coe_toOrthonormalBasis_repr`, `toBasis_toOrthonormalBasis`, `coe_toOrthonormalBasis_repr_symm`, `coe_toOrthonormalBasis`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toOrthonormalBasis` 📖	mathematical	`Orthonormal` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `Module.Basis` `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` `instFunLike`	`DFunLike.coe` `OrthonormalBasis` `OrthonormalBasis.instFunLike` `toOrthonormalBasis` `Module.Basis` `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` `instFunLike`	—	`OrthonormalBasis.coe_toBasis` `toBasis_toOrthonormalBasis`
`coe_toOrthonormalBasis_repr` 📖	mathematical	`Orthonormal` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `Module.Basis` `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` `instFunLike`	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EuclideanSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PiLp.seminormedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `RCLike.innerProductSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `OrthonormalBasis.repr` `toOrthonormalBasis` `LinearEquiv` `WithLp` `Nat.instAtLeastTwoHAddOfNat` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedRing.toRing` `NormedCommRing.toNormedRing` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.trans` `Pi.addCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `RingHomCompTriple.ids` `equivFun` `Finite.of_fintype` `LinearEquiv.symm` `WithLp.linearEquiv`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal`
`coe_toOrthonormalBasis_repr_symm` 📖	mathematical	`Orthonormal` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `Module.Basis` `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` `instFunLike`	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EuclideanSpace` `PiLp.seminormedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `OrthonormalBasis.repr` `toOrthonormalBasis` `LinearEquiv` `WithLp` `Nat.instAtLeastTwoHAddOfNat` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedRing.toRing` `NormedCommRing.toNormedRing` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.trans` `RingHomCompTriple.ids` `WithLp.linearEquiv` `LinearEquiv.symm` `Pi.addCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `equivFun` `Finite.of_fintype`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal`
`toBasis_toOrthonormalBasis` 📖	mathematical	`Orthonormal` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `Module.Basis` `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` `instFunLike`	`OrthonormalBasis.toBasis` `toOrthonormalBasis`	—	`ofEquivFun_equivFun` `Finite.of_fintype`

Orthonormal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_orthonormalBasis_extension` 📖	mathematical	`Orthonormal` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set` `Set.instMembership`	`Finset` `OrthonormalBasis` `SetLike.instMembership` `Finset.instSetLike` `Finset.Subtype.fintype` `Set` `Set.instHasSubset` `SetLike.coe` `DFunLike.coe` `OrthonormalBasis.instFunLike`	—	`exists_maximal_orthonormal` `LinearIndependent.setFinite` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `linearIndependent` `comp` `Equiv.injective` `Subtype.range_coe_subtype` `Submodule.HasOrthogonalProjection.ofCompleteSpace` `complete_of_proper` `FiniteDimensional.RCLike.properSpace_submodule` `FiniteDimensional.finiteDimensional_submodule` `maximal_orthonormal_iff_orthogonalComplement_eq_bot` `Set.Finite.coe_toFinset`
`exists_orthonormalBasis_extension_of_card_eq` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Fintype.card` `Orthonormal` `Set.Elem` `Set.restrict`	`OrthonormalBasis` `DFunLike.coe` `OrthonormalBasis.instFunLike`	—	`LinearIndependent.injective` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `linearIndependent` `orthonormal_subtype_range` `exists_orthonormalBasis_extension` `Module.finrank_eq_card_finset_basis` `commRing_strongRankCondition` `Set.MapsTo.mono_right` `Set.mapsTo_image` `Set.range_restrict` `Set.injOn_iff_injective` `Set.MapsTo.exists_equiv_extend_of_card_eq` `OrthonormalBasis.coe_reindex`

OrthonormalBasis

Definitions

Name	Category	Theorems
`equiv` 📖	CompOp	6 math math: `equiv_apply`, `equiv_self_rfl`, `equiv_apply_euclideanSpace`, `equiv_symm`, `equiv_apply_basis`, `coe_equiv_euclideanSpace`
`fromOrthogonalSpanSingleton` 📖	CompOp	—
`instFunLike` 📖	CompOp	100 math math: `Orthonormal.exists_orthonormalBasis_extension_of_card_eq`, `orthogonalProjection_eq_sum`, `nnnorm_eq_one`, `sum_inner_mul_inner`, `orthogonalProjection_eq_sum_rankOne`, `det_to_matrix_orthonormalBasis_of_same_orientation`, `EuclideanSpace.basisFun_apply`, `InnerProductSpace.canonicalCovariantTensor_eq_sum`, `det_to_matrix_orthonormalBasis_of_opposite_orientation`, `Matrix.IsHermitian.eigenvalues_eq`, `repr_self`, `sum_sq_inner_right`, `Complex.coe_orthonormalBasisOneI`, `Matrix.IsHermitian.eigenvectorUnitary_col_eq`, `Orientation.abs_volumeForm_apply_of_orthonormal`, `ProbabilityTheory.covarianceBilin_apply_basisFun_self`, `LinearMap.toMatrixOrthonormal_apply_apply`, `coe_reindex`, `Matrix.IsHermitian.eigenvectorUnitary_mulVec`, `prod_apply`, `orthogonalProjection_apply_eq_sum`, `LinearMap.trace_eq_sum_inner`, `DirectSum.IsInternal.subordinateOrthonormalBasis_subordinate`, `InnerProductSpace.gramSchmidtOrthonormalBasis_apply`, `orthonormalBasis_one_dim`, `coe_ofRepr`, `norm_eq_one`, `Pi.orthonormalBasis_apply`, `sum_sq_norm_inner_right`, `starProjection_eq_sum_rankOne`, `singleton_apply`, `equiv_apply`, `volume_parallelepiped`, `repr_apply_apply`, `sum_sq_inner_left`, `reindex_apply`, `LinearMap.toMatrix_innerₛₗ_apply`, `LineDeriv.laplacianCLM_eq_sum`, `coe_mk`, `coe_of_orthogonal_eq_bot_mk`, `det_to_matrix_orthonormalBasis`, `InnerProductSpace.gramSchmidtOrthonormalBasis_apply_of_orthogonal`, `coe_toBasis`, `exists_orthonormalBasis`, `InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis`, `tensorProduct_apply'`, `InnerProductSpace.gramSchmidtOrthonormalBasis_det`, `sum_sq_norm_inner_left`, `equiv_apply_euclideanSpace`, `inner_eq_zero`, `TemperedDistribution.laplacian_eq_sum`, `Matrix.IsHermitian.eigenvectorUnitary_apply`, `map_apply`, `sum_repr_symm`, `InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis`, `ProbabilityTheory.covarianceBilin_apply_basisFun`, `DirectSum.IsInternal.collectedOrthonormalBasis_mem`, `enorm_eq_one`, `InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis`, `EuclideanSpace.basisFun_inner`, `orthonormal`, `LinearMap.IsSymmetric.apply_eigenvectorBasis`, `EuclideanSpace.inner_basisFun_real`, `repr_symm_single`, `toMatrix_innerSL_apply`, `equiv_apply_basis`, `norm_le_card_mul_iSup_norm_inner`, `span_apply`, `toMatrix_orthonormalBasis_mem_unitary`, `adjustToOrientation_apply_eq_or_eq_neg`, `Module.Basis.coe_toOrthonormalBasis`, `InnerProductSpace.inner_gramSchmidtOrthonormalBasis_eq_zero`, `norm_dual`, `Complex.isometryOfOrthonormal_apply`, `SchwartzMap.laplacian_eq_sum`, `InnerProductSpace.gramSchmidtOrthonormalBasis_inv_triangular`, `inner_eq_one`, `ProbabilityTheory.stdGaussian_eq_map_pi_orthonormalBasis`, `InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis`, `sum_repr`, `LineDeriv.tensorLineDerivTwo_canonicalCovariantTensor_eq_sum`, `sum_rankOne_eq_id`, `coe_toHilbertBasis`, `coe_equiv_euclideanSpace`, `Matrix.IsHermitian.eigenvectorUnitary_transpose_apply`, `toMatrix_orthonormalBasis_self_mul_conjTranspose`, `HilbertBasis.coe_toOrthonormalBasis`, `toMatrix_orthonormalBasis_conjTranspose_mul_self`, `toMatrix_orthonormalBasis_mem_orthogonal`, `coe_singleton`, `tensorProduct_apply`, `det_to_matrix_orthonormalBasis_real`, `Orthonormal.exists_orthonormalBasis_extension`, `Matrix.IsHermitian.mulVec_eigenvectorBasis`, `parallelepiped_orthonormalBasis_one_dim`, `sum_repr'`, `LinearMap.IsSymmetric.hasEigenvector_eigenvectorBasis`, `Matrix.IsHermitian.star_eigenvectorUnitary_mulVec`, `Orientation.measure_orthonormalBasis`, `inner_eq_ite`
`instInhabited` 📖	CompOp	—
`map` 📖	CompOp	3 math math: `toBasis_map`, `map_apply`, `Complex.map_isometryOfOrthonormal`
`mk` 📖	CompOp	—
`mkOfOrthogonalEqBot` 📖	CompOp	1 math math: `coe_of_orthogonal_eq_bot_mk`
`reindex` 📖	CompOp	7 math math: `LinearMap.toMatrixOrthonormal_reindex`, `coe_reindex`, `reindex_apply`, `DirectSum.IsInternal.subordinateOrthonormalBasis_def`, `reindex_toBasis`, `repr_reindex`, `LinearMap.IsSymmetric.eigenvectorBasis_def`
`repr` 📖	CompOp	27 math math: `singleton_repr`, `repr_injective`, `repr_self`, `measurePreserving_repr`, `Module.Basis.coe_toOrthonormalBasis_repr`, `Matrix.gram_eq_conjTranspose_mul`, `Complex.orthonormalBasisOneI_repr_apply`, `tensorProduct_repr_tmul_apply'`, `equiv_apply`, `Module.Basis.coe_toOrthonormalBasis_repr_symm`, `repr_apply_apply`, `LinearMap.toMatrix_innerₛₗ_apply`, `LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply`, `EuclideanSpace.basisFun_repr`, `Complex.orthonormalBasisOneI_repr_symm_apply`, `sum_repr_symm`, `measurePreserving_repr_symm`, `InnerProductSpace.toMatrix_rankOne`, `repr_symm_single`, `toMatrix_innerSL_apply`, `InnerProductSpace.gramSchmidtOrthonormalBasis_inv_triangular'`, `coe_toBasis_repr`, `sum_repr`, `coe_toBasis_repr_apply`, `Pi.orthonormalBasis_repr`, `repr_reindex`, `tensorProduct_repr_tmul_apply`
`singleton` 📖	CompOp	4 math math: `singleton_repr`, `toBasis_singleton`, `singleton_apply`, `coe_singleton`
`span` 📖	CompOp	1 math math: `span_apply`
`toBasis` 📖	CompOp	51 math math: `Orientation.volumeForm_robust_neg`, `toBasis_tensorProduct`, `EuclideanSpace.basisFun_toBasis`, `det_to_matrix_orthonormalBasis_of_same_orientation`, `det_eq_neg_det_of_opposite_orientation`, `det_to_matrix_orthonormalBasis_of_opposite_orientation`, `toBasis_singleton`, `Complex.toBasis_orthonormalBasisOneI`, `toBasis_adjustToOrientation`, `LinearMap.isHermitian_toMatrix_iff`, `NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq`, `Orientation.volumeForm_def`, `Orientation.volumeForm_robust`, `toBasis_mulOpposite`, `Module.Basis.toBasis_toOrthonormalBasis`, `toBasis_map`, `LinearMap.toMatrixOrthonormal_symm_apply`, `LinearMap.toMatrix_innerₛₗ_apply`, `det_to_matrix_orthonormalBasis`, `coe_toBasis`, `InnerProductSpace.gramSchmidtOrthonormalBasis_det`, `det_adjustToOrientation`, `LinearMap.toMatrixOrthonormal_apply`, `Pi.orthonormalBasis.toBasis`, `Matrix.toLin_conjTranspose`, `InnerProductSpace.gramSchmidtOrthonormalBasis_inv_blockTriangular`, `Matrix.IsHermitian.eigenvectorUnitary_coe`, `InnerProductSpace.toMatrix_rankOne`, `reindex_toBasis`, `Matrix.isSymmetric_toLin_iff`, `orthonormal_adjustToOrientation`, `toMatrix_innerSL_apply`, `Orientation.volumeForm_robust'`, `toMatrix_orthonormalBasis_mem_unitary`, `coe_toBasis_repr`, `coe_toBasis_repr_apply`, `LinearIsometryEquiv.toMatrix_mem_unitaryGroup`, `same_orientation_iff_det_eq_det`, `Orientation.finOrthonormalBasis_orientation`, `toMatrix_orthonormalBasis_self_mul_conjTranspose`, `toMatrix_orthonormalBasis_conjTranspose_mul_self`, `toMatrix_orthonormalBasis_mem_orthogonal`, `orientation_adjustToOrientation`, `Matrix.toEuclideanLin_eq_toLin_orthonormal`, `Complex.isometryOfOrthonormal_symm_apply`, `addHaar_eq_volume`, `det_to_matrix_orthonormalBasis_real`, `LinearMap.toMatrix_adjoint`, `LinearMap.IsSymmetric.toMatrix_eigenvectorBasis`, `LinearMap.posSemidef_toMatrix_iff`, `abs_det_adjustToOrientation`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_equiv_euclideanSpace` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EuclideanSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `PiLp.innerProductSpace` `RCLike.innerProductSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `equiv` `EuclideanSpace.basisFun` `Equiv.refl` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `WithLp.ofLp` `OrthonormalBasis` `instFunLike`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `Finset.sum_congr`
`coe_mk` 📖	mathematical	`Orthonormal` `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` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Top.top` `Submodule.instTop` `Submodule.span` `Set.range`	`DFunLike.coe` `OrthonormalBasis` `instFunLike`	—	`Module.Basis.coe_toOrthonormalBasis`
`coe_ofRepr` 📖	mathematical	—	`DFunLike.coe` `OrthonormalBasis` `instFunLike` `ofRepr` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EuclideanSpace` `PiLp.seminormedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `EuclideanSpace.single` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable`
`coe_of_orthogonal_eq_bot_mk` 📖	mathematical	`Orthonormal` `NormedAddCommGroup.toSeminormedAddCommGroup` `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` `Set.range` `Bot.bot` `Submodule` `Submodule.instBot`	`DFunLike.coe` `OrthonormalBasis` `instFunLike` `mkOfOrthogonalEqBot`	—	—
`coe_reindex` 📖	mathematical	—	`DFunLike.coe` `OrthonormalBasis` `instFunLike` `reindex` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	`reindex_apply`
`coe_singleton` 📖	mathematical	—	`DFunLike.coe` `OrthonormalBasis` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.innerProductSpace` `Unique.fintype` `instFunLike` `singleton` `Pi.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`singleton_apply`
`coe_toBasis` 📖	mathematical	—	`DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Module.Basis.instFunLike` `toBasis` `OrthonormalBasis` `instFunLike`	—	—
`coe_toBasis_repr` 📖	mathematical	—	`Module.Basis.equivFun` `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` `Finite.of_fintype` `toBasis` `LinearEquiv.trans` `EuclideanSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `PiLp.seminormedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Pi.addCommGroup` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `WithLp.instModule` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `RCLike.innerProductSpace` `NormedRing.toRing` `NormedCommRing.toNormedRing` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `RingHomInvPair.ids` `LinearIsometryEquiv.toLinearEquiv` `repr` `WithLp.linearEquiv` `Nat.instAtLeastTwoHAddOfNat`	—	`Module.Basis.equivFun_ofEquivFun` `Finite.of_fintype` `fact_one_le_two_ennreal`
`coe_toBasis_repr_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `toBasis` `WithLp.ofLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `LinearIsometryEquiv` `EuclideanSpace` `PiLp.seminormedAddCommGroup` `fact_one_le_two_ennreal` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `RCLike.innerProductSpace` `LinearIsometryEquiv.instEquivLike` `repr`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `Nat.instAtLeastTwoHAddOfNat` `Finite.of_fintype` `RingHomCompTriple.ids` `coe_toBasis_repr`
`det_to_matrix_orthonormalBasis` 📖	mathematical	—	`Norm.norm` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `DFunLike.coe` `AlternatingMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedField.toField` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `AlternatingMap.instFunLike` `Module.Basis.det` `toBasis` `OrthonormalBasis` `instFunLike` `Real` `Real.instOne`	—	`Matrix.det_of_mem_unitary` `toMatrix_orthonormalBasis_mem_unitary` `pow_eq_one_iff_of_nonneg` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instZeroLEOneClass` `norm_nonneg` `two_ne_zero` `Nat.cast_one` `algebraMap.coe_one` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.of_divisionRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `RCLike.mul_conj` `RCLike.star_def`
`det_to_matrix_orthonormalBasis_real` 📖	mathematical	—	`DFunLike.coe` `AlternatingMap` `Real` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Real.commRing` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `InnerProductSpace.toNormedSpace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule` `AlternatingMap.instFunLike` `Module.Basis.det` `toBasis` `OrthonormalBasis` `instFunLike` `Real.instOne` `Real.instNeg`	—	`sq_eq_one_iff` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `sq` `TrivialStar.star_trivial` `instTrivialStarReal` `Matrix.det_of_mem_unitary` `toMatrix_orthonormalBasis_mem_unitary`
`enorm_eq_one` 📖	mathematical	—	`ENorm.enorm` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `DFunLike.coe` `OrthonormalBasis` `instFunLike` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`Orthonormal.enorm_eq_one` `orthonormal`
`equiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `equiv` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `WithLp.ofLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `EuclideanSpace` `PiLp.seminormedAddCommGroup` `fact_one_le_two_ennreal` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `RCLike.innerProductSpace` `repr` `OrthonormalBasis` `instFunLike` `Equiv` `Equiv.instEquivLike`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `sum_repr` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `SemilinearIsometryEquivClass.toSemilinearIsometryClass` `LinearIsometryEquiv.instSemilinearIsometryEquivClass` `Finset.sum_congr` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `equiv_apply_basis`
`equiv_apply_basis` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `equiv` `OrthonormalBasis` `instFunLike` `Equiv` `Equiv.instEquivLike`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `repr_self` `DFunLike.congr` `PiLp.ext` `LinearIsometryEquiv.piLpCongrLeft_single` `PiLp.single_apply`
`equiv_apply_euclideanSpace` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EuclideanSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PiLp.normedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `PiLp.innerProductSpace` `RCLike.innerProductSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `equiv` `EuclideanSpace.basisFun` `Equiv.refl` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `WithLp.ofLp` `OrthonormalBasis` `instFunLike`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `Finset.sum_congr` `equiv_apply`
`equiv_self_rfl` 📖	mathematical	—	`equiv` `Equiv.refl` `LinearIsometryEquiv.refl` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace`	—	`Module.Basis.ext_linearIsometryEquiv` `RingHomInvPair.ids` `equiv_apply_basis`
`equiv_symm` 📖	mathematical	—	`LinearIsometryEquiv.symm` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `equiv` `Equiv.symm`	—	`Module.Basis.ext_linearIsometryEquiv` `RingHomInvPair.ids` `fact_one_le_two_ennreal` `LinearIsometryEquiv.trans.congr_simp` `LinearIsometryEquiv.piLpCongrLeft_symm`
`inner_eq_ite` 📖	mathematical	—	`Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `OrthonormalBasis` `instFunLike` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing`	—	`inner_self_eq_norm_sq_to_K` `norm_eq_one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_pow` `inner_eq_zero`
`inner_eq_one` 📖	mathematical	—	`Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `OrthonormalBasis` `instFunLike` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField`	—	`inner_self_eq_norm_sq_to_K` `norm_eq_one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_pow`
`inner_eq_zero` 📖	mathematical	—	`Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `OrthonormalBasis` `instFunLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField`	—	`Orthonormal.inner_eq_zero` `orthonormal`
`map_apply` 📖	mathematical	—	`DFunLike.coe` `OrthonormalBasis` `instFunLike` `map` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike`	—	`RingHomInvPair.ids`
`nnnorm_eq_one` 📖	mathematical	—	`NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `OrthonormalBasis` `instFunLike` `NNReal` `NNReal.instOne`	—	`Orthonormal.nnnorm_eq_one` `orthonormal`
`norm_eq_one` 📖	mathematical	—	`Norm.norm` `NormedAddCommGroup.toNorm` `DFunLike.coe` `OrthonormalBasis` `instFunLike` `Real` `Real.instOne`	—	`Orthonormal.norm_eq_one` `orthonormal`
`norm_le_card_mul_iSup_norm_inner` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `Real.instMul` `Real.sqrt` `Real.instNatCast` `Fintype.card` `iSup` `Real.instSupSet` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `OrthonormalBasis` `instFunLike`	—	`sum_sq_norm_inner_right` `Real.sqrt_sq` `norm_nonneg` `Real.sqrt_monotone` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `pow_le_pow_left₀` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `le_ciSup` `Finite.of_fintype` `instIsDirectedOrder` `Real.instArchimedean` `Finset.sum_const` `nsmul_eq_mul` `Real.sqrt_mul` `isEmpty_or_nonempty` `Real.iSup_of_isEmpty` `instReflLe` `le_ciSup_of_le`
`orthogonalProjection_apply_eq_sum` 📖	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` `Submodule.setLike` `instTopologicalSpaceSubtype` `Submodule.addCommMonoid` `Submodule.module` `ContinuousLinearMap.funLike` `Submodule.orthogonalProjection` `Finset.sum` `Finset.univ` `Submodule.smul` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Inner.inner` `InnerProductSpace.toInner` `OrthonormalBasis` `Submodule.normedAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule.innerProductSpace` `instFunLike`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `Finset.sum_congr` `repr_apply_apply` `Submodule.inner_orthogonalProjection_eq_of_mem_left` `sum_repr`
`orthogonalProjection_eq_sum` 📖	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` `Submodule.setLike` `instTopologicalSpaceSubtype` `Submodule.addCommMonoid` `Submodule.module` `ContinuousLinearMap.funLike` `Submodule.orthogonalProjection` `Finset.sum` `Finset.univ` `Submodule.smul` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Inner.inner` `InnerProductSpace.toInner` `OrthonormalBasis` `Submodule.normedAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule.innerProductSpace` `instFunLike`	—	`orthogonalProjection_apply_eq_sum`
`orthogonalProjection_eq_sum_rankOne` 📖	mathematical	—	`Submodule.orthogonalProjection` `Finset.sum` `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` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Submodule` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `SetLike.instMembership` `Submodule.setLike` `Submodule.seminormedAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule.normedSpace` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Submodule.normedAddCommGroup` `Submodule.topologicalAddGroup` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Finset.univ` `DFunLike.coe` `starRingEnd` `RCLike.toStarRing` `ContinuousLinearMap.topologicalSpace` `SeminormedAddGroup.toAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.funLike` `ContinuousLinearMap.addCommGroup` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `DenselyNormedField.toNontriviallyNormedField` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `ContinuousLinearMap.continuousConstSMul` `InnerProductSpace.rankOne` `OrthonormalBasis` `Submodule.innerProductSpace` `instFunLike`	—	`ContinuousLinearMap.ext` `IsScalarTower.left` `IsTopologicalAddGroup.toContinuousAdd` `Submodule.topologicalAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.topologicalAddGroup` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `ContinuousLinearMap.continuousConstSMul` `orthogonalProjection_apply_eq_sum` `AddSubmonoidClass.coe_finset_sum` `Submodule.addSubmonoidClass` `Finset.sum_congr` `ContinuousLinearMap.coe_sum'` `Finset.sum_apply` `Submodule.addSubgroupClass`
`orthonormal` 📖	mathematical	—	`Orthonormal` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `OrthonormalBasis` `instFunLike`	—	`orthonormal_iff_ite` `fact_one_le_two_ennreal` `RingHomInvPair.ids` `LinearIsometryEquiv.inner_map_map` `repr_self` `Nat.instAtLeastTwoHAddOfNat` `EuclideanSpace.inner_single_left` `PiLp.single_apply` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_mul`
`reindex_apply` 📖	mathematical	—	`DFunLike.coe` `OrthonormalBasis` `instFunLike` `reindex` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	`fact_one_le_two_ennreal` `RingHomInvPair.ids` `coe_ofRepr` `repr_symm_single` `LinearIsometryEquiv.piLpCongrLeft_symm` `Nat.instAtLeastTwoHAddOfNat` `EuclideanSpace.piLpCongrLeft_single`
`reindex_toBasis` 📖	mathematical	—	`toBasis` `reindex` `Module.Basis.reindex` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace`	—	`Module.Basis.eq_ofRepr_eq_repr` `RingHomInvPair.ids`
`repr_apply_apply` 📖	mathematical	—	`WithLp.ofLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EuclideanSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PiLp.seminormedAddCommGroup` `fact_one_le_two_ennreal` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `RCLike.innerProductSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `repr` `Inner.inner` `InnerProductSpace.toInner` `OrthonormalBasis` `instFunLike`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `LinearIsometryEquiv.inner_map_map` `repr_self` `Nat.instAtLeastTwoHAddOfNat` `EuclideanSpace.inner_single_left` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_mul`
`repr_injective` 📖	mathematical	—	`OrthonormalBasis` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EuclideanSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PiLp.seminormedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `RCLike.innerProductSpace` `repr`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal`
`repr_reindex` 📖	mathematical	—	`WithLp.ofLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EuclideanSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PiLp.seminormedAddCommGroup` `fact_one_le_two_ennreal` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `RCLike.innerProductSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `repr` `reindex` `Equiv` `Equiv.instEquivLike` `Equiv.symm`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `repr_apply_apply` `coe_reindex`
`repr_self` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EuclideanSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PiLp.seminormedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `RCLike.innerProductSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `repr` `OrthonormalBasis` `instFunLike` `EuclideanSpace.single` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `repr_symm_single` `LinearIsometryEquiv.apply_symm_apply`
`repr_symm_single` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EuclideanSpace` `PiLp.seminormedAddCommGroup` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `fact_one_le_two_ennreal` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedAddCommGroup.toSeminormedAddCommGroup` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `repr` `EuclideanSpace.single` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `OrthonormalBasis` `instFunLike`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable`
`singleton_apply` 📖	mathematical	—	`DFunLike.coe` `OrthonormalBasis` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.innerProductSpace` `Unique.fintype` `instFunLike` `singleton` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`Module.Basis.singleton_apply`
`singleton_repr` 📖	mathematical	—	`WithLp.ofLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EuclideanSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `PiLp.seminormedAddCommGroup` `fact_one_le_two_ennreal` `Unique.fintype` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `repr` `singleton`	—	`Module.Basis.singleton_repr`
`span_apply` 📖	mathematical	`Orthonormal` `NormedAddCommGroup.toSeminormedAddCommGroup`	`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.span` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.image` `DFunLike.coe` `OrthonormalBasis` `Submodule.normedAddCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `Submodule.innerProductSpace` `Finset.Subtype.fintype` `instFunLike` `span`	—	`RingHomInvPair.ids` `Submodule.subset_span` `Set.mem_range_self` `Module.Basis.span_apply`
`starProjection_eq_sum_rankOne` 📖	mathematical	—	`Submodule.starProjection` `Finset.sum` `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` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Finset.univ` `DFunLike.coe` `starRingEnd` `Semifield.toCommSemiring` `RCLike.toStarRing` `ContinuousLinearMap.topologicalSpace` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `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` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.funLike` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `DenselyNormedField.toNontriviallyNormedField` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `ContinuousLinearMap.continuousConstSMul` `InnerProductSpace.rankOne` `Submodule` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `OrthonormalBasis` `Submodule.normedAddCommGroup` `Submodule.innerProductSpace` `instFunLike`	—	`ContinuousLinearMap.ext` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.topologicalAddGroup` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `ContinuousLinearMap.continuousConstSMul` `IsScalarTower.left` `Submodule.topologicalAddGroup` `ContinuousLinearMap.comp.congr_simp` `orthogonalProjection_eq_sum_rankOne` `ContinuousLinearMap.coe_sum'` `Finset.sum_apply` `Finset.sum_congr` `AddSubmonoidClass.coe_finset_sum` `Submodule.addSubgroupClass`
`sum_inner_mul_inner` 📖	mathematical	—	`Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Finset.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `OrthonormalBasis` `instFunLike`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `RingHomInvPair.ids` `fact_one_le_two_ennreal` `sum_repr` `Finset.sum_congr` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `repr_apply_apply` `mul_comm` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass`
`sum_rankOne_eq_id` 📖	mathematical	—	`Finset.sum` `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` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Finset.univ` `DFunLike.coe` `starRingEnd` `Semifield.toCommSemiring` `RCLike.toStarRing` `ContinuousLinearMap.topologicalSpace` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `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` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.funLike` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `DenselyNormedField.toNontriviallyNormedField` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `ContinuousLinearMap.continuousConstSMul` `InnerProductSpace.rankOne` `OrthonormalBasis` `instFunLike` `ContinuousLinearMap.id` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`ContinuousLinearMap.ext` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.topologicalAddGroup` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `ContinuousLinearMap.continuousConstSMul` `ContinuousLinearMap.coe_sum'` `Finset.sum_apply` `Finset.sum_congr` `sum_repr'`
`sum_repr` 📖	mathematical	—	`Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Module.toDistribMulAction` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `WithLp.ofLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `DFunLike.coe` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EuclideanSpace` `PiLp.seminormedAddCommGroup` `fact_one_le_two_ennreal` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `RCLike.innerProductSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `repr` `OrthonormalBasis` `instFunLike`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `Finset.sum_congr` `coe_toBasis_repr_apply` `Module.Basis.sum_repr`
`sum_repr'` 📖	mathematical	—	`Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Module.toDistribMulAction` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Inner.inner` `InnerProductSpace.toInner` `DFunLike.coe` `OrthonormalBasis` `instFunLike`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `sum_repr` `Finset.sum_congr` `repr_apply_apply`
`sum_repr_symm` 📖	mathematical	—	`Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Module.toDistribMulAction` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `WithLp.ofLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `DFunLike.coe` `OrthonormalBasis` `instFunLike` `LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EuclideanSpace` `PiLp.seminormedAddCommGroup` `fact_one_le_two_ennreal` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `RCLike.innerProductSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `repr`	—	`RingHomInvPair.ids` `fact_one_le_two_ennreal` `Finset.sum_congr` `Finite.of_fintype` `RingHomCompTriple.ids` `Nat.instAtLeastTwoHAddOfNat` `coe_toBasis_repr` `Module.Basis.equivFun_symm_apply`
`sum_sq_inner_left` 📖	mathematical	—	`Finset.sum` `Real` `Real.instAddCommMonoid` `Finset.univ` `Monoid.toPow` `Real.instMonoid` `Inner.inner` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `OrthonormalBasis` `instFunLike` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`sum_sq_inner_right` `Finset.sum_congr` `real_inner_comm`
`sum_sq_inner_right` 📖	mathematical	—	`Finset.sum` `Real` `Real.instAddCommMonoid` `Finset.univ` `Monoid.toPow` `Real.instMonoid` `Inner.inner` `InnerProductSpace.toInner` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `OrthonormalBasis` `instFunLike` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`sum_sq_norm_inner_right` `Finset.sum_congr` `sq_abs`
`sum_sq_norm_inner_left` 📖	mathematical	—	`Finset.sum` `Real` `Real.instAddCommMonoid` `Finset.univ` `Monoid.toPow` `Real.instMonoid` `Norm.norm` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `OrthonormalBasis` `instFunLike` `NormedAddCommGroup.toNorm`	—	`Finset.sum_congr` `inner_conj_symm` `RCLike.norm_conj` `sum_sq_norm_inner_right`
`sum_sq_norm_inner_right` 📖	mathematical	—	`Finset.sum` `Real` `Real.instAddCommMonoid` `Finset.univ` `Monoid.toPow` `Real.instMonoid` `Norm.norm` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Inner.inner` `InnerProductSpace.toInner` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `OrthonormalBasis` `instFunLike` `NormedAddCommGroup.toNorm`	—	`norm_eq_sqrt_re_inner` `sum_inner_mul_inner` `map_sum` `AddMonoidHom.instAddMonoidHomClass` `Finset.sum_congr` `inner_mul_symm_re_eq_norm` `norm_mul` `NormedDivisionRing.toNormMulClass` `inner_conj_symm` `norm_star` `CStarRing.to_normedStarGroup` `RCLike.instCStarRing` `Real.sq_sqrt` `Fintype.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `Nat.instAtLeastTwoHAddOfNat` `even_two_mul`
`toBasis_map` 📖	mathematical	—	`toBasis` `map` `Module.Basis.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` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `LinearIsometryEquiv.toLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids`	—	`RingHomInvPair.ids`
`toBasis_singleton` 📖	mathematical	—	`toBasis` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.innerProductSpace` `Unique.fintype` `singleton` `Module.Basis.singleton` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField`	—	`Module.Basis.toBasis_toOrthonormalBasis`
`toMatrix_orthonormalBasis_conjTranspose_mul_self` 📖	mathematical	—	`Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `Matrix.conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `RCLike.toStarRing` `Module.Basis.toMatrix` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `toBasis` `DFunLike.coe` `OrthonormalBasis` `instFunLike` `Matrix.one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`Matrix.ext` `fact_one_le_two_ennreal` `RingHomInvPair.ids` `Nat.instAtLeastTwoHAddOfNat` `Finset.sum_congr` `RCLike.inner_apply'` `orthonormal_iff_ite` `orthonormal` `Matrix.one_apply` `LinearIsometryEquiv.inner_map_map`
`toMatrix_orthonormalBasis_mem_orthogonal` 📖	mathematical	—	`Matrix` `Real` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Real.commRing` `SetLike.instMembership` `Submonoid.instSetLike` `Matrix.orthogonalGroup` `Module.Basis.toMatrix` `Real.instCommSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Real.instRCLike` `InnerProductSpace.toNormedSpace` `toBasis` `DFunLike.coe` `OrthonormalBasis` `instFunLike`	—	`toMatrix_orthonormalBasis_mem_unitary`
`toMatrix_orthonormalBasis_mem_unitary` 📖	mathematical	—	`Matrix` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Matrix.nonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `SetLike.instMembership` `Submonoid.instSetLike` `Matrix.unitaryGroup` `RCLike.toStarRing` `Module.Basis.toMatrix` `Semifield.toCommSemiring` `Field.toSemifield` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `toBasis` `DFunLike.coe` `OrthonormalBasis` `instFunLike`	—	`Matrix.mem_unitaryGroup_iff'` `toMatrix_orthonormalBasis_conjTranspose_mul_self`
`toMatrix_orthonormalBasis_self_mul_conjTranspose` 📖	mathematical	—	`Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `Module.Basis.toMatrix` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `toBasis` `DFunLike.coe` `OrthonormalBasis` `instFunLike` `Matrix.conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `RCLike.toStarRing` `Matrix.one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`Matrix.mul_eq_one_comm_of_equiv` `instIsStablyFiniteRingOfOrzechProperty` `CommRing.orzechProperty` `invariantBasisNumber_of_nontrivial_of_commRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `toMatrix_orthonormalBasis_conjTranspose_mul_self`

Pi

Definitions

Name	Category	Theorems
`orthonormalBasis` 📖	CompOp	3 math math: `orthonormalBasis_apply`, `orthonormalBasis.toBasis`, `orthonormalBasis_repr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`orthonormalBasis_apply` 📖	mathematical	—	`DFunLike.coe` `OrthonormalBasis` `PiLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `PiLp.innerProductSpace` `Sigma.instFintype` `OrthonormalBasis.instFunLike` `orthonormalBasis` `PiLp.single` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`PiLp.ext` `Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `RingHomInvPair.ids` `OrthonormalBasis.coe_ofRepr` `Sigma.curry_single` `Decidable.eq_or_ne` `single_eq_same` `OrthonormalBasis.repr_symm_single` `single_eq_of_ne'` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearIsometryClass.toSemilinearMapClass` `SemilinearIsometryEquivClass.toSemilinearIsometryClass` `LinearIsometryEquiv.instSemilinearIsometryEquivClass`
`orthonormalBasis_repr` 📖	mathematical	—	`WithLp.ofLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `PiLp` `Nat.instAtLeastTwoHAddOfNat` `EuclideanSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `PiLp.seminormedAddCommGroup` `Sigma.instFintype` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `PiLp.innerProductSpace` `WithLp.instModule` `addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `RCLike.innerProductSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `OrthonormalBasis.repr` `orthonormalBasis` `WithLp.toLp`	—	`RingHomInvPair.ids` `Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal`

Pi.orthonormalBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toBasis` 📖	mathematical	—	`OrthonormalBasis.toBasis` `PiLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `PiLp.innerProductSpace` `Sigma.instFintype` `Pi.orthonormalBasis` `Module.Basis.map` `WithLp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Pi.module` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `AddCommGroup.toAddCommMonoid` `WithLp.instAddCommGroup` `Pi.addCommGroup` `NormedAddCommGroup.toAddCommGroup` `WithLp.instModule` `Pi.basis` `LinearEquiv.symm` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `WithLp.linearEquiv`	—	`Module.Basis.eq_of_apply_eq` `Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `RingHomInvPair.ids` `PiLp.ext`

PiLp

Definitions

Name	Category	Theorems
`innerProductSpace` 📖	CompOp	76 math math: `Matrix.l2_opNorm_toEuclideanCLM`, `Pi.comul_eq_adjoint`, `EuclideanSpace.orthonormal_single`, `Matrix.cstar_nnnorm_def`, `ProbabilityTheory.covarianceBilin_multivariateGaussian`, `EuclideanSpace.inner_single_left`, `EuclideanSpace.basisFun_toBasis`, `GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace`, `EuclideanSpace.basisFun_apply`, `Matrix.IsHermitian.eigenvalues_eq`, `OrthonormalBasis.measurePreserving_repr`, `Matrix.IsHermitian.eigenvectorUnitary_col_eq`, `ProbabilityTheory.charFun_multivariateGaussian`, `Pi.counit_eq_adjoint`, `ProbabilityTheory.covarianceBilin_apply_basisFun_self`, `LDL.lowerInv_orthogonal`, `GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace`, `EuclideanSpace.volume_closedBall_fin_three`, `NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq`, `Matrix.IsHermitian.eigenvectorUnitary_mulVec`, `volume_preserving_toLp`, `InnerProductGeometry.norm_toLp_symm_crossProduct`, `Matrix.toEuclideanCLM_toLp`, `EuclideanSpace.volume_closedBall_fin_two`, `Pi.orthonormalBasis_apply`, `Matrix.isSymmetric_toEuclideanLin_iff`, `ProbabilityTheory.map_pi_eq_stdGaussian`, `MeasureTheory.charFun_pi`, `NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed`, `RCLike.wInner_one_eq_inner`, `Matrix.inner_toEuclideanCLM`, `volume_preserving_ofLp`, `InnerProductGeometry.norm_ofLp_crossProduct`, `Matrix.ofLp_toEuclideanCLM`, `Matrix.isPositive_toEuclideanLin_iff`, `EuclideanSpace.basisFun_repr`, `OrthonormalBasis.equiv_apply_euclideanSpace`, `Matrix.coe_toEuclideanCLM_eq_toEuclideanLin`, `Matrix.IsHermitian.eigenvectorUnitary_apply`, `ProbabilityTheory.covarianceBilin_apply_pi`, `EuclideanSpace.inner_eq_star_dotProduct`, `Pi.orthonormalBasis.toBasis`, `EuclideanSpace.volume_ball_fin_three`, `ProbabilityTheory.covarianceBilin_apply_basisFun`, `OrthonormalBasis.measurePreserving_repr_symm`, `Matrix.IsHermitian.eigenvectorUnitary_coe`, `Matrix.isHermitian_iff_isSymmetric`, `EuclideanSpace.basisFun_inner`, `Matrix.toEuclideanLin_conjTranspose_eq_adjoint`, `EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp`, `EuclideanSpace.volume_ball_fin_two`, `EuclideanSpace.inner_basisFun_real`, `EuclideanSpace.volume_ball`, `ProbabilityTheory.iIndepFun_iff_charFun_pi`, `volume_euclideanSpace_eq_dirac`, `OrthonormalBasis.coe_equiv_euclideanSpace`, `EuclideanSpace.inner_toLp_toLp`, `Matrix.IsHermitian.eigenvectorUnitary_transpose_apply`, `ProbabilityTheory.multivariateGaussian_zero_one`, `inner_apply`, `NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm`, `EuclideanSpace.inner_single_right`, `Matrix.toEuclideanLin_eq_toLin_orthonormal`, `EuclideanSpace.euclideanHausdorffMeasure_eq_volume`, `Matrix.cstar_norm_def`, `inner_matrix_row_row`, `Matrix.IsHermitian.mulVec_eigenvectorBasis`, `OrthonormalBasis.measurePreserving_measurableEquiv`, `Pi.orthonormalBasis_repr`, `MeasureTheory.charFun_eq_pi_iff`, `EuclideanSpace.volume_closedBall`, `Matrix.IsHermitian.star_eigenvectorUnitary_mulVec`, `InnerProductSpace.symm_toEuclideanLin_rankOne`, `MeasureTheory.Measure.euclideanHausdorffMeasure_def`, `RCLike.inner_eq_wInner_one`, `inner_matrix_col_col`
`vecNotation` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inner_apply` 📖	mathematical	—	`Inner.inner` `PiLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `InnerProductSpace.toInner` `seminormedAddCommGroup` `fact_one_le_two_ennreal` `NormedAddCommGroup.toSeminormedAddCommGroup` `innerProductSpace` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Finset.univ` `WithLp.ofLp`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal`

(root)

Definitions

Name	Category	Theorems
`OrthonormalBasis` 📖	CompData	101 math math: `Orthonormal.exists_orthonormalBasis_extension_of_card_eq`, `OrthonormalBasis.orthogonalProjection_eq_sum`, `OrthonormalBasis.repr_injective`, `OrthonormalBasis.nnnorm_eq_one`, `OrthonormalBasis.sum_inner_mul_inner`, `OrthonormalBasis.orthogonalProjection_eq_sum_rankOne`, `OrthonormalBasis.det_to_matrix_orthonormalBasis_of_same_orientation`, `EuclideanSpace.basisFun_apply`, `InnerProductSpace.canonicalCovariantTensor_eq_sum`, `OrthonormalBasis.det_to_matrix_orthonormalBasis_of_opposite_orientation`, `Matrix.IsHermitian.eigenvalues_eq`, `OrthonormalBasis.repr_self`, `OrthonormalBasis.sum_sq_inner_right`, `Complex.coe_orthonormalBasisOneI`, `Matrix.IsHermitian.eigenvectorUnitary_col_eq`, `Orientation.abs_volumeForm_apply_of_orthonormal`, `ProbabilityTheory.covarianceBilin_apply_basisFun_self`, `LinearMap.toMatrixOrthonormal_apply_apply`, `OrthonormalBasis.coe_reindex`, `Matrix.IsHermitian.eigenvectorUnitary_mulVec`, `OrthonormalBasis.prod_apply`, `OrthonormalBasis.orthogonalProjection_apply_eq_sum`, `LinearMap.trace_eq_sum_inner`, `DirectSum.IsInternal.subordinateOrthonormalBasis_subordinate`, `InnerProductSpace.gramSchmidtOrthonormalBasis_apply`, `orthonormalBasis_one_dim`, `OrthonormalBasis.coe_ofRepr`, `OrthonormalBasis.norm_eq_one`, `Pi.orthonormalBasis_apply`, `OrthonormalBasis.sum_sq_norm_inner_right`, `OrthonormalBasis.starProjection_eq_sum_rankOne`, `OrthonormalBasis.singleton_apply`, `OrthonormalBasis.equiv_apply`, `OrthonormalBasis.volume_parallelepiped`, `OrthonormalBasis.repr_apply_apply`, `OrthonormalBasis.sum_sq_inner_left`, `OrthonormalBasis.reindex_apply`, `LinearMap.toMatrix_innerₛₗ_apply`, `LineDeriv.laplacianCLM_eq_sum`, `OrthonormalBasis.coe_mk`, `OrthonormalBasis.coe_of_orthogonal_eq_bot_mk`, `OrthonormalBasis.det_to_matrix_orthonormalBasis`, `InnerProductSpace.gramSchmidtOrthonormalBasis_apply_of_orthogonal`, `OrthonormalBasis.coe_toBasis`, `exists_orthonormalBasis`, `InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_orthonormalBasis`, `OrthonormalBasis.tensorProduct_apply'`, `InnerProductSpace.gramSchmidtOrthonormalBasis_det`, `OrthonormalBasis.sum_sq_norm_inner_left`, `OrthonormalBasis.equiv_apply_euclideanSpace`, `OrthonormalBasis.inner_eq_zero`, `TemperedDistribution.laplacian_eq_sum`, `Matrix.IsHermitian.eigenvectorUnitary_apply`, `OrthonormalBasis.map_apply`, `OrthonormalBasis.sum_repr_symm`, `InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis`, `ProbabilityTheory.covarianceBilin_apply_basisFun`, `DirectSum.IsInternal.collectedOrthonormalBasis_mem`, `OrthonormalBasis.enorm_eq_one`, `InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis`, `EuclideanSpace.basisFun_inner`, `OrthonormalBasis.orthonormal`, `LinearMap.IsSymmetric.apply_eigenvectorBasis`, `EuclideanSpace.inner_basisFun_real`, `OrthonormalBasis.repr_symm_single`, `toMatrix_innerSL_apply`, `OrthonormalBasis.equiv_apply_basis`, `OrthonormalBasis.norm_le_card_mul_iSup_norm_inner`, `OrthonormalBasis.span_apply`, `OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary`, `OrthonormalBasis.adjustToOrientation_apply_eq_or_eq_neg`, `Module.Basis.coe_toOrthonormalBasis`, `InnerProductSpace.inner_gramSchmidtOrthonormalBasis_eq_zero`, `OrthonormalBasis.norm_dual`, `Complex.isometryOfOrthonormal_apply`, `SchwartzMap.laplacian_eq_sum`, `InnerProductSpace.gramSchmidtOrthonormalBasis_inv_triangular`, `OrthonormalBasis.inner_eq_one`, `ProbabilityTheory.stdGaussian_eq_map_pi_orthonormalBasis`, `InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis`, `OrthonormalBasis.sum_repr`, `LineDeriv.tensorLineDerivTwo_canonicalCovariantTensor_eq_sum`, `OrthonormalBasis.sum_rankOne_eq_id`, `OrthonormalBasis.coe_toHilbertBasis`, `OrthonormalBasis.coe_equiv_euclideanSpace`, `Matrix.IsHermitian.eigenvectorUnitary_transpose_apply`, `OrthonormalBasis.toMatrix_orthonormalBasis_self_mul_conjTranspose`, `HilbertBasis.coe_toOrthonormalBasis`, `OrthonormalBasis.toMatrix_orthonormalBasis_conjTranspose_mul_self`, `OrthonormalBasis.toMatrix_orthonormalBasis_mem_orthogonal`, `OrthonormalBasis.coe_singleton`, `OrthonormalBasis.tensorProduct_apply`, `OrthonormalBasis.det_to_matrix_orthonormalBasis_real`, `Orthonormal.exists_orthonormalBasis_extension`, `Matrix.IsHermitian.mulVec_eigenvectorBasis`, `parallelepiped_orthonormalBasis_one_dim`, `OrthonormalBasis.sum_repr'`, `LinearMap.IsSymmetric.hasEigenvector_eigenvectorBasis`, `Matrix.IsHermitian.star_eigenvectorUnitary_mulVec`, `Orientation.measure_orthonormalBasis`, `OrthonormalBasis.inner_eq_ite`
`stdOrthonormalBasis` 📖	CompOp	4 math math: `stdOrthonormalBasis_def`, `InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis`, `DirectSum.IsInternal.subordinateOrthonormalBasis_def`, `InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_orthonormalBasis` 📖	mathematical	—	`Finset` `OrthonormalBasis` `SetLike.instMembership` `Finset.instSetLike` `Finset.Subtype.fintype` `DFunLike.coe` `OrthonormalBasis.instFunLike`	—	`Orthonormal.exists_orthonormalBasis_extension` `orthonormal_empty`
`finrank_euclideanSpace` 📖	mathematical	—	`Module.finrank` `EuclideanSpace` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `Fintype.card`	—	`fact_one_le_two_ennreal` `Nat.instAtLeastTwoHAddOfNat` `Module.finrank_fintype_fun_eq_card` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `LinearEquiv.finrank_eq`
`finrank_euclideanSpace_fin` 📖	mathematical	—	`Module.finrank` `EuclideanSpace` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `ESeminormedAddCommMonoid.toAddCommMonoid` `PiLp.topologicalSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `PiLp.normedAddCommGroup` `fact_one_le_two_ennreal` `Fin.fintype` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `WithLp.instModule` `Pi.addCommGroup` `SeminormedAddCommGroup.toAddCommGroup` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace`	—	`fact_one_le_two_ennreal` `finrank_euclideanSpace` `Fintype.card_fin`
`inner_matrix_col_col` 📖	mathematical	—	`Inner.inner` `WithLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `InnerProductSpace.toInner` `PiLp.seminormedAddCommGroup` `fact_one_le_two_ennreal` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `PiLp.innerProductSpace` `RCLike.innerProductSpace` `WithLp.toLp` `Matrix.transpose` `Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Matrix.conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `RCLike.toStarRing`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `Finset.sum_congr` `mul_comm`
`inner_matrix_row_row` 📖	mathematical	—	`Inner.inner` `WithLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `InnerProductSpace.toInner` `PiLp.seminormedAddCommGroup` `fact_one_le_two_ennreal` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `PiLp.innerProductSpace` `RCLike.innerProductSpace` `WithLp.toLp` `Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Matrix.conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `RCLike.toStarRing`	—	`Nat.instAtLeastTwoHAddOfNat` `fact_one_le_two_ennreal` `Finset.sum_congr`
`orthonormalBasis_one_dim` 📖	mathematical	—	`DFunLike.coe` `OrthonormalBasis` `Real` `Real.instRCLike` `Real.normedAddCommGroup` `RCLike.toInnerProductSpaceReal` `OrthonormalBasis.instFunLike` `Real.instOne` `Real.instNeg`	—	`commRing_strongRankCondition` `Real.instNontrivial` `OrthonormalBasis.orthonormal` `abs_eq` `Real.instIsOrderedAddMonoid` `zero_le_one'` `Real.instZeroLEOneClass` `Real.norm_eq_abs` `eq_const_of_unique`
`stdOrthonormalBasis_def` 📖	mathematical	—	`stdOrthonormalBasis`	—	`exists_orthonormalBasis`
`toMatrix_innerSL_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `Matrix` `LinearMap.addCommMonoid` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Matrix.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearMap.toMatrix` `Finite.of_fintype` `OrthonormalBasis.toBasis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `starRingEnd` `RCLike.toStarRing` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `Algebra.to_smulCommClass` `Algebra.id` `LinearMap.instFunLike` `innerₛₗ` `Matrix.vecMulVec` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `Star.star` `Pi.instStarForall` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid` `OrthonormalBasis` `OrthonormalBasis.instFunLike` `WithLp.ofLp` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `LinearIsometryEquiv` `EuclideanSpace` `PiLp.seminormedAddCommGroup` `fact_one_le_two_ennreal` `WithLp.instModule` `Pi.addCommGroup` `Pi.Function.module` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `LinearIsometryEquiv.instEquivLike` `OrthonormalBasis.repr`	—	`LinearMap.toMatrix_innerₛₗ_apply`

---

← Back to Index