Orthonormal

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

Statistics

Metric	Count
Definitions `isometryOfOrthonormal`, `isometryOfOrthonormal`, `Orthonormal`, `equiv`, `basisOfOrthonormalOfCardEqFinrank`	5
Theorems `coe_isometryOfOrthonormal`, `isometryOfOrthonormal_toLinearEquiv`, `orthonormal_comp_iff`, `coe_isometryOfOrthonormal`, `isometryOfOrthonormal_toLinearMap`, `comp`, `comp_linearIsometry`, `comp_linearIsometryEquiv`, `enorm_eq_one`, `equiv_apply`, `equiv_refl`, `equiv_symm`, `equiv_toLinearEquiv`, `equiv_trans`, `inner_eq_zero`, `inner_finsupp_eq_sum_left`, `inner_finsupp_eq_sum_right`, `inner_finsupp_eq_zero`, `inner_left_finsupp`, `inner_left_fintype`, `inner_left_right_finset`, `inner_left_sum`, `inner_products_summable`, `inner_right_finsupp`, `inner_right_fintype`, `inner_right_sum`, `inner_sum`, `linearIndependent`, `mapLinearIsometryEquiv`, `map_equiv`, `ne_zero`, `nnnorm_eq_one`, `norm_eq_one`, `of_isEmpty`, `orthonormal_of_forall_eq_or_eq_neg`, `sum_inner_products_le`, `toSubtypeRange`, `tsum_inner_products_le`, `coe_basisOfOrthonormalOfCardEqFinrank`, `exists_maximal_orthonormal`, `orthonormal_empty`, `orthonormal_iUnion_of_directed`, `orthonormal_iff_ite`, `orthonormal_sUnion_of_directed`, `orthonormal_subtype_iff_ite`, `orthonormal_subtype_range`, `orthonormal_vecCons_iff`	47
Total	52

LinearEquiv

Definitions

Name	Category	Theorems
`isometryOfOrthonormal` 📖	CompOp	2 math math: `coe_isometryOfOrthonormal`, `isometryOfOrthonormal_toLinearEquiv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_isometryOfOrthonormal` 📖	mathematical	`Orthonormal` `DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Module.Basis.instFunLike` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv`	`LinearIsometryEquiv` `LinearIsometryEquiv.instEquivLike` `isometryOfOrthonormal`	—	`RingHomInvPair.ids`
`isometryOfOrthonormal_toLinearEquiv` 📖	mathematical	`Orthonormal` `DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Module.Basis.instFunLike` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv`	`LinearIsometryEquiv.toLinearEquiv` `isometryOfOrthonormal`	—	`RingHomInvPair.ids`

LinearIsometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`orthonormal_comp_iff` 📖	mathematical	—	`Orthonormal` `DFunLike.coe` `LinearIsometry` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `instFunLike`	—	`inner_map_map`

LinearMap

Definitions

Name	Category	Theorems
`isometryOfOrthonormal` 📖	CompOp	2 math math: `coe_isometryOfOrthonormal`, `isometryOfOrthonormal_toLinearMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_isometryOfOrthonormal` 📖	mathematical	`Orthonormal` `DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Module.Basis.instFunLike` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike`	`LinearIsometry` `LinearIsometry.instFunLike` `isometryOfOrthonormal`	—	—
`isometryOfOrthonormal_toLinearMap` 📖	mathematical	`Orthonormal` `DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Module.Basis.instFunLike` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instFunLike`	`LinearIsometry.toLinearMap` `isometryOfOrthonormal`	—	—

Orthonormal

Definitions

Name	Category	Theorems
`equiv` 📖	CompOp	6 math math: `equiv_symm`, `equiv_trans`, `map_equiv`, `equiv_toLinearEquiv`, `equiv_refl`, `equiv_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`Orthonormal`	—	—	`orthonormal_iff_ite`
`comp_linearIsometry` 📖	mathematical	`Orthonormal`	`DFunLike.coe` `LinearIsometry` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `LinearIsometry.instFunLike`	—	`LinearIsometry.orthonormal_comp_iff`
`comp_linearIsometryEquiv` 📖	mathematical	`Orthonormal`	`DFunLike.coe` `LinearIsometryEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike`	—	`RingHomInvPair.ids` `comp_linearIsometry`
`enorm_eq_one` 📖	mathematical	`Orthonormal`	`ENorm.enorm` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddGroup.toContinuousENorm` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`ofReal_norm` `norm_eq_one` `ENNReal.ofReal_one`
`equiv_apply` 📖	mathematical	`Orthonormal` `DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Module.Basis.instFunLike`	`LinearIsometryEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `equiv` `Equiv` `Equiv.instEquivLike`	—	`Module.Basis.equiv_apply`
`equiv_refl` 📖	mathematical	`Orthonormal` `DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Module.Basis.instFunLike`	`equiv` `Equiv.refl` `LinearIsometryEquiv.refl`	—	`Module.Basis.ext_linearIsometryEquiv` `RingHomInvPair.ids` `equiv_apply`
`equiv_symm` 📖	mathematical	`Orthonormal` `DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Module.Basis.instFunLike`	`LinearIsometryEquiv.symm` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `equiv` `Equiv.symm`	—	`Module.Basis.ext_linearIsometryEquiv` `RingHomInvPair.ids` `LinearIsometryEquiv.injective` `LinearIsometryEquiv.apply_symm_apply` `equiv_apply` `Equiv.apply_symm_apply`
`equiv_toLinearEquiv` 📖	mathematical	`Orthonormal` `DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Module.Basis.instFunLike`	`LinearIsometryEquiv.toLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `equiv` `Module.Basis.equiv`	—	`RingHomInvPair.ids`
`equiv_trans` 📖	mathematical	`Orthonormal` `DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Module.Basis.instFunLike`	`LinearIsometryEquiv.trans` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `RingHomCompTriple.ids` `equiv` `Equiv.trans`	—	`Module.Basis.ext_linearIsometryEquiv` `RingHomInvPair.ids` `RingHomCompTriple.ids` `equiv_apply` `Equiv.coe_trans`
`inner_eq_zero` 📖	mathematical	`Orthonormal`	`Inner.inner` `InnerProductSpace.toInner` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField`	—	—
`inner_finsupp_eq_sum_left` 📖	mathematical	`Orthonormal`	`Inner.inner` `InnerProductSpace.toInner` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Finsupp.module` `Semiring.toModule` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `LinearMap.instFunLike` `Finsupp.linearCombination` `Finsupp.sum` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `RingHom` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `RingHom.instFunLike` `starRingEnd` `RCLike.toStarRing` `Finsupp.instFunLike`	—	`Finsupp.linearCombination_apply` `Finsupp.sum_inner` `inner_smul_left` `inner_right_finsupp`
`inner_finsupp_eq_sum_right` 📖	mathematical	`Orthonormal`	`Inner.inner` `InnerProductSpace.toInner` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Finsupp.module` `Semiring.toModule` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `LinearMap.instFunLike` `Finsupp.linearCombination` `Finsupp.sum` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `RingHom` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `RingHom.instFunLike` `starRingEnd` `RCLike.toStarRing` `Finsupp.instFunLike`	—	`Finsupp.linearCombination_apply` `Finsupp.inner_sum` `inner_smul_right` `inner_left_finsupp` `mul_comm`
`inner_finsupp_eq_zero` 📖	mathematical	`Orthonormal` `Set` `Set.instMembership` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Submodule` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Finsupp.instAddCommMonoid` `Finsupp.module` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace` `SetLike.instMembership` `Submodule.setLike` `Finsupp.supported`	`Inner.inner` `InnerProductSpace.toInner` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Semiring.toModule` `LinearMap.instFunLike` `Finsupp.linearCombination`	—	`inner_left_finsupp` `Finsupp.mem_supported'` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`inner_left_finsupp` 📖	mathematical	`Orthonormal`	`Inner.inner` `InnerProductSpace.toInner` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Finsupp.module` `Semiring.toModule` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `LinearMap.instFunLike` `Finsupp.linearCombination` `RingHom` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `RingHom.instFunLike` `starRingEnd` `RCLike.toStarRing` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Finsupp.instFunLike`	—	`inner_conj_symm` `inner_right_finsupp`
`inner_left_fintype` 📖	mathematical	`Orthonormal`	`Inner.inner` `InnerProductSpace.toInner` `Finset.sum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `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` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `RingHom.instFunLike` `starRingEnd` `RCLike.toStarRing`	—	`inner_left_sum` `Finset.mem_univ`
`inner_left_right_finset` 📖	mathematical	`Orthonormal`	`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` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `CommSemiring.toSemiring` `Algebra.id` `Inner.inner` `InnerProductSpace.toInner`	—	`Finset.sum_congr` `orthonormal_iff_ite` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `Finset.sum_ite_eq'` `Finset.sum_ite_mem` `Finset.inter_self`
`inner_left_sum` 📖	mathematical	`Orthonormal` `Finset` `Finset.instMembership`	`Inner.inner` `InnerProductSpace.toInner` `Finset.sum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `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` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `RingHom.instFunLike` `starRingEnd` `RCLike.toStarRing`	—	`sum_inner` `Finset.sum_congr` `inner_smul_left` `orthonormal_iff_ite` `mul_boole` `Finset.sum_ite_eq'`
`inner_products_summable` 📖	mathematical	`Orthonormal`	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Inner.inner` `InnerProductSpace.toInner` `SummationFilter.unconditional`	—	`hasSum_of_isLUB_of_nonneg` `Real.instIsOrderedAddMonoid` `instOrderTopologyReal` `Real.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `isLUB_ciSup` `sum_inner_products_le`
`inner_right_finsupp` 📖	mathematical	`Orthonormal`	`Inner.inner` `InnerProductSpace.toInner` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Finsupp.module` `Semiring.toModule` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `LinearMap.instFunLike` `Finsupp.linearCombination` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Finsupp.instFunLike`	—	`Finsupp.inner_sum` `inner_smul_right` `orthonormal_iff_ite` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `Finsupp.sum_ite_eq`
`inner_right_fintype` 📖	mathematical	`Orthonormal`	`Inner.inner` `InnerProductSpace.toInner` `Finset.sum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `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_right_sum` `Finset.mem_univ`
`inner_right_sum` 📖	mathematical	`Orthonormal` `Finset` `Finset.instMembership`	`Inner.inner` `InnerProductSpace.toInner` `Finset.sum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `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_sum` `Finset.sum_congr` `inner_smul_right` `orthonormal_iff_ite` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `Finset.sum_ite_eq`
`inner_sum` 📖	mathematical	`Orthonormal`	`Inner.inner` `InnerProductSpace.toInner` `Finset.sum` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `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` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `RingHom.instFunLike` `starRingEnd` `RCLike.toStarRing`	—	`sum_inner` `Finset.sum_congr` `inner_smul_left` `inner_right_sum`
`linearIndependent` 📖	mathematical	`Orthonormal`	`LinearIndependent` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace`	—	`linearIndependent_iff` `Finsupp.ext` `inner_right_finsupp` `inner_zero_right`
`mapLinearIsometryEquiv` 📖	mathematical	`Orthonormal` `DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Module.Basis.instFunLike`	`Module.Basis.map` `LinearIsometryEquiv.toLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids`	—	`RingHomInvPair.ids` `comp_linearIsometryEquiv`
`map_equiv` 📖	mathematical	`Orthonormal` `DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace` `Module.Basis.instFunLike`	`Module.Basis.map` `LinearIsometryEquiv.toLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `equiv` `Module.Basis.reindex` `Equiv.symm`	—	`Module.Basis.map_equiv`
`ne_zero` 📖	—	`Orthonormal`	—	—	`norm_zero` `NeZero.charZero_one` `RCLike.charZero_rclike`
`nnnorm_eq_one` 📖	mathematical	`Orthonormal`	`NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NNReal` `instOneNNReal`	—	`norm_eq_one` `Nat.cast_one`
`norm_eq_one` 📖	mathematical	`Orthonormal`	`Norm.norm` `SeminormedAddCommGroup.toNorm` `Real` `Real.instOne`	—	—
`of_isEmpty` 📖	mathematical	—	`Orthonormal`	—	`Subsingleton.pairwise` `IsEmpty.instSubsingleton`
`orthonormal_of_forall_eq_or_eq_neg` 📖	—	`Orthonormal` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	—	`orthonormal_iff_ite` `inner_neg_right` `inner_neg_left` `neg_neg`
`sum_inner_products_le` 📖	mathematical	`Orthonormal`	`Real` `Real.instLE` `Finset.sum` `Real.instAddCommMonoid` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Inner.inner` `InnerProductSpace.toInner` `SeminormedAddCommGroup.toNorm`	—	`inner_left_right_finset` `RCLike.mul_conj` `RCLike.ofReal_re` `Nat.instAtLeastTwoHAddOfNat` `norm_sub_sq` `sub_add` `InnerProductSpace.norm_sq_eq_re_inner` `inner_sum` `Finset.sum_congr` `sum_inner` `inner_smul_right` `two_mul` `inner_smul_left` `inner_conj_symm` `add_sub_cancel_right` `map_sum` `AddMonoidHom.instAddMonoidHomClass` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing`
`toSubtypeRange` 📖	mathematical	`Orthonormal`	`Set` `Set.instMembership` `Set.range`	—	`orthonormal_subtype_range` `LinearIndependent.injective` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `linearIndependent`
`tsum_inner_products_le` 📖	mathematical	`Orthonormal`	`Real` `Real.instLE` `tsum` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `Inner.inner` `InnerProductSpace.toInner` `SummationFilter.unconditional` `SeminormedAddCommGroup.toNorm`	—	`tsum_le_of_sum_le'` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `sum_inner_products_le`

(root)

Definitions

Name	Category	Theorems
`Orthonormal` 📖	MathDef	16 math math: `EuclideanSpace.orthonormal_single`, `orthonormal_subtype_range`, `InnerProductSpace.gramSchmidtNormed_orthonormal`, `orthonormal_empty`, `Module.Basis.mulOpposite_is_orthonormal_iff`, `orthonormal_fourier`, `UnitAddTorus.orthonormal_mFourier`, `orthonormal_subtype_iff_ite`, `LinearIsometry.orthonormal_comp_iff`, `HilbertBasis.orthonormal`, `OrthonormalBasis.orthonormal_adjustToOrientation`, `OrthonormalBasis.orthonormal`, `Orthonormal.of_isEmpty`, `orthonormal_iff_ite`, `orthonormal_vecCons_iff`, `InnerProductSpace.gramSchmidtNormed_orthonormal'`
`basisOfOrthonormalOfCardEqFinrank` 📖	CompOp	1 math math: `coe_basisOfOrthonormalOfCardEqFinrank`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_basisOfOrthonormalOfCardEqFinrank` 📖	mathematical	`Orthonormal` `Fintype.card` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `InnerProductSpace.toNormedSpace`	`DFunLike.coe` `Module.Basis` `Module.Basis.instFunLike` `basisOfOrthonormalOfCardEqFinrank`	—	`coe_basisOfLinearIndependentOfCardEqFinrank` `Orthonormal.linearIndependent`
`exists_maximal_orthonormal` 📖	mathematical	`Orthonormal` `Set` `Set.instMembership`	`Set.instHasSubset`	—	`zorn_subset_nonempty` `orthonormal_sUnion_of_directed` `IsChain.directedOn` `Set.instReflSubset` `Set.subset_sUnion_of_mem` `Maximal.eq_of_ge`
`orthonormal_empty` 📖	mathematical	—	`Orthonormal` `Set.Elem` `Set` `Set.instEmptyCollection` `Set.instMembership`	—	`Set.instIsEmptyElemEmptyCollection`
`orthonormal_iUnion_of_directed` 📖	mathematical	`Directed` `Set` `Set.instHasSubset` `Orthonormal` `Set.Elem` `Set.instMembership`	`Set.iUnion`	—	`orthonormal_subtype_iff_ite`
`orthonormal_iff_ite` 📖	mathematical	—	`Orthonormal` `Inner.inner` `InnerProductSpace.toInner` `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` `Orthonormal.norm_eq_one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_pow` `Orthonormal.inner_eq_zero` `InnerProductSpace.norm_sq_eq_re_inner` `RCLike.one_re` `norm_nonneg` `zero_le_one` `Real.instZeroLEOneClass` `sq_eq_sq₀` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing`
`orthonormal_sUnion_of_directed` 📖	mathematical	`DirectedOn` `Set` `Set.instHasSubset` `Orthonormal` `Set.Elem` `Set.instMembership`	`Set.sUnion`	—	`Set.sUnion_eq_iUnion` `orthonormal_iUnion_of_directed` `DirectedOn.directed_val`
`orthonormal_subtype_iff_ite` 📖	mathematical	—	`Orthonormal` `Set` `Set.instMembership` `Inner.inner` `InnerProductSpace.toInner` `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`	—	`orthonormal_iff_ite`
`orthonormal_subtype_range` 📖	mathematical	—	`Orthonormal` `Set` `Set.instMembership` `Set.range`	—	`Orthonormal.comp` `Equiv.injective` `Equiv.self_comp_ofInjective_symm`
`orthonormal_vecCons_iff` 📖	mathematical	—	`Orthonormal` `Matrix.vecCons` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real` `Real.instOne` `Inner.inner` `InnerProductSpace.toInner` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField`	—	`instSymmEqInnerOfNat`

---

← Back to Index