GramSchmidtOrtho

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

Statistics

Metric	Count
Definitions gramSchmidt, gramSchmidtBasis, gramSchmidtNormed, gramSchmidtOrthonormalBasis	4
Theorems coe_gramSchmidtBasis, gramSchmidtNormed_linearIndependent, gramSchmidtNormed_orthonormal, gramSchmidtNormed_orthonormal', gramSchmidtNormed_unit_length, gramSchmidtNormed_unit_length', gramSchmidtNormed_unit_length_coe, gramSchmidtOrthonormalBasis_apply, gramSchmidtOrthonormalBasis_apply_of_orthogonal, gramSchmidtOrthonormalBasis_det, gramSchmidtOrthonormalBasis_inv_blockTriangular, gramSchmidtOrthonormalBasis_inv_triangular, gramSchmidtOrthonormalBasis_inv_triangular', gramSchmidt_bot, gramSchmidt_def, gramSchmidt_def', gramSchmidt_def'', gramSchmidt_inv_triangular, gramSchmidt_linearIndependent, gramSchmidt_mem_span, gramSchmidt_ne_zero, gramSchmidt_ne_zero_coe, gramSchmidt_of_orthogonal, gramSchmidt_orthogonal, gramSchmidt_pairwise_orthogonal, gramSchmidt_triangular, gramSchmidt_zero, inner_gramSchmidtOrthonormalBasis_eq_zero, mem_span_gramSchmidt, span_gramSchmidt, span_gramSchmidtNormed, span_gramSchmidtNormed_range, span_gramSchmidt_Iic, span_gramSchmidt_Iio	34
Total	38

InnerProductSpace

Definitions

Name	Category	Theorems
gramSchmidt 📖	CompOp	19 math math: span_gramSchmidtNormed, span_gramSchmidtNormed_range, gramSchmidt_bot, gramSchmidt_def, gramSchmidt_of_orthogonal, gramSchmidt_orthogonal, gramSchmidt_pairwise_orthogonal, coe_gramSchmidtBasis, gramSchmidt_triangular, gramSchmidt_def', span_gramSchmidt_Iic, gramSchmidt_def'', mem_span_gramSchmidt, gramSchmidt_zero, span_gramSchmidt, span_gramSchmidt_Iio, gramSchmidt_linearIndependent, gramSchmidt_mem_span, gramSchmidt_inv_triangular
gramSchmidtBasis 📖	CompOp	2 math math: LDL.lowerInv_eq_gramSchmidtBasis, coe_gramSchmidtBasis
gramSchmidtNormed 📖	CompOp	9 math math: span_gramSchmidtNormed, gramSchmidtNormed_orthonormal, span_gramSchmidtNormed_range, gramSchmidtNormed_unit_length_coe, gramSchmidtNormed_linearIndependent, gramSchmidtOrthonormalBasis_apply, gramSchmidtNormed_unit_length, gramSchmidtNormed_unit_length', gramSchmidtNormed_orthonormal'
gramSchmidtOrthonormalBasis 📖	CompOp	7 math math: gramSchmidtOrthonormalBasis_apply, gramSchmidtOrthonormalBasis_apply_of_orthogonal, gramSchmidtOrthonormalBasis_det, gramSchmidtOrthonormalBasis_inv_blockTriangular, gramSchmidtOrthonormalBasis_inv_triangular', inner_gramSchmidtOrthonormalBasis_eq_zero, gramSchmidtOrthonormalBasis_inv_triangular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_gramSchmidtBasis 📖	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 toNormedSpace Module.Basis.instFunLike gramSchmidtBasis gramSchmidt	—	—
gramSchmidtNormed_linearIndependent 📖	mathematical	LinearIndependent 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 toNormedSpace	gramSchmidtNormed	—	isUnit_iff_ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass gramSchmidt_ne_zero LinearIndependent.units_smul gramSchmidt_linearIndependent
gramSchmidtNormed_orthonormal 📖	mathematical	LinearIndependent 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 toNormedSpace	Orthonormal gramSchmidtNormed	—	gramSchmidtNormed_unit_length inner_smul_right inner_smul_left RCLike.conj_inv RCLike.conj_ofReal NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass gramSchmidt_orthogonal
gramSchmidtNormed_orthonormal' 📖	mathematical	—	Orthonormal NormedAddCommGroup.toSeminormedAddCommGroup Set.Elem setOf gramSchmidtNormed NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup Set Set.instMembership	—	gramSchmidtNormed_unit_length' Subtype.prop inner_smul_right inner_smul_left map_inv₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RCLike.conj_ofReal gramSchmidt_orthogonal MulZeroClass.mul_zero
gramSchmidtNormed_unit_length 📖	mathematical	LinearIndependent 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 toNormedSpace	Norm.norm NormedAddCommGroup.toNorm gramSchmidtNormed Real Real.instOne	—	gramSchmidtNormed_unit_length_coe LinearIndependent.comp Subtype.coe_injective
gramSchmidtNormed_unit_length' 📖	mathematical	—	Norm.norm NormedAddCommGroup.toNorm gramSchmidtNormed Real Real.instOne	—	gramSchmidtNormed.eq_1 norm_smul_inv_norm instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero IsLocalRing.toNontrivial Field.instIsLocalRing RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
gramSchmidtNormed_unit_length_coe 📖	mathematical	LinearIndependent Set Set.instMembership Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 toNormedSpace	Norm.norm NormedAddCommGroup.toNorm gramSchmidtNormed Real Real.instOne	—	norm_smul_inv_norm gramSchmidt_ne_zero_coe
gramSchmidtOrthonormalBasis_apply 📖	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 toNormedSpace Fintype.card	DFunLike.coe OrthonormalBasis OrthonormalBasis.instFunLike gramSchmidtOrthonormalBasis gramSchmidtNormed	—	Orthonormal.exists_orthonormalBasis_extension_of_card_eq gramSchmidtNormed_orthonormal'
gramSchmidtOrthonormalBasis_apply_of_orthogonal 📖	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 toNormedSpace Fintype.card Pairwise Inner.inner toInner MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing	DFunLike.coe OrthonormalBasis OrthonormalBasis.instFunLike gramSchmidtOrthonormalBasis SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero RCLike.ofReal Norm.norm NormedAddCommGroup.toNorm	—	gramSchmidtNormed.eq_1 gramSchmidt_of_orthogonal gramSchmidtOrthonormalBasis_apply instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors instIsDomain GroupWithZero.toNoZeroSMulDivisors IsDomain.toIsCancelMulZero IsLocalRing.toNontrivial Field.instIsLocalRing RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
gramSchmidtOrthonormalBasis_det 📖	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 toNormedSpace Fintype.card	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule AlternatingMap.instFunLike Module.Basis.det OrthonormalBasis.toBasis gramSchmidtOrthonormalBasis Finset.prod CommRing.toCommMonoid Finset.univ Inner.inner toInner OrthonormalBasis OrthonormalBasis.instFunLike	—	Finset.prod_congr RingHomInvPair.ids fact_one_le_two_ennreal OrthonormalBasis.repr_apply_apply Matrix.det_of_upperTriangular gramSchmidtOrthonormalBasis_inv_blockTriangular
gramSchmidtOrthonormalBasis_inv_blockTriangular 📖	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 toNormedSpace Fintype.card	Matrix.BlockTriangular Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing Module.Basis.toMatrix Semifield.toCommSemiring OrthonormalBasis.toBasis gramSchmidtOrthonormalBasis	—	gramSchmidtOrthonormalBasis_inv_triangular'
gramSchmidtOrthonormalBasis_inv_triangular 📖	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 toNormedSpace Fintype.card Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Inner.inner toInner DFunLike.coe OrthonormalBasis OrthonormalBasis.instFunLike gramSchmidtOrthonormalBasis MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing	—	inner_gramSchmidtOrthonormalBasis_eq_zero gramSchmidtOrthonormalBasis_apply inner_smul_left map_inv₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RCLike.conj_ofReal gramSchmidt_inv_triangular MulZeroClass.mul_zero
gramSchmidtOrthonormalBasis_inv_triangular' 📖	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 toNormedSpace Fintype.card Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	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 OrthonormalBasis.repr gramSchmidtOrthonormalBasis MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing	—	RingHomInvPair.ids fact_one_le_two_ennreal OrthonormalBasis.repr_apply_apply gramSchmidtOrthonormalBasis_inv_triangular
gramSchmidt_bot 📖	mathematical	—	gramSchmidt LocallyFiniteOrder.toLocallyFiniteOrderBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Bot.bot OrderBot.toBot Preorder.toLE	—	Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton gramSchmidt_def Finset.Iio_eq_Ico Finset.Ico_self Finset.sum_empty sub_zero
gramSchmidt_def 📖	mathematical	—	gramSchmidt SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Finset.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring NormedSpace.toModule toNormedSpace ContinuousLinearMap.funLike Submodule.starProjection Submodule.span Set Set.instSingletonSet Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper Submodule SetLike.instMembership Submodule.setLike Subtype.pseudoMetricSpace FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing SeminormedAddCommGroup.toAddCommGroup	—	Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton Finset.sum_attach Finset.attach_eq_univ gramSchmidt.eq_1
gramSchmidt_def' 📖	mathematical	—	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid gramSchmidt Finset.sum Finset.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring NormedSpace.toModule toNormedSpace ContinuousLinearMap.funLike Submodule.starProjection Submodule.span Set Set.instSingletonSet Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper Submodule SetLike.instMembership Submodule.setLike Subtype.pseudoMetricSpace FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing SeminormedAddCommGroup.toAddCommGroup	—	Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton gramSchmidt_def sub_add_cancel
gramSchmidt_def'' 📖	mathematical	—	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid gramSchmidt Finset.sum Finset.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 toNormedSpace DivInvMonoid.toDiv DivisionRing.toDivInvMonoid NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Inner.inner toInner Monoid.toNatPow RCLike.ofReal Norm.norm NormedAddCommGroup.toNorm	—	Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton Finset.sum_congr MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass gramSchmidt_def'
gramSchmidt_inv_triangular 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Inner.inner toInner NormedAddCommGroup.toSeminormedAddCommGroup gramSchmidt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	gramSchmidt_def'' inner_add_right inner_sum Finset.sum_congr inner_smul_right gramSchmidt_orthogonal LT.lt.ne' Finset.sum_eq_zero LT.lt.trans MulZeroClass.mul_zero zero_add
gramSchmidt_linearIndependent 📖	mathematical	LinearIndependent 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 toNormedSpace	gramSchmidt	—	linearIndependent_of_ne_zero_of_inner_eq_zero gramSchmidt_ne_zero gramSchmidt_orthogonal
gramSchmidt_mem_span 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	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 toNormedSpace SetLike.instMembership Submodule.setLike Submodule.span Set.image Set.Iic gramSchmidt	—	—
gramSchmidt_ne_zero 📖	—	LinearIndependent 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 toNormedSpace	—	—	gramSchmidt_ne_zero_coe LinearIndependent.comp Subtype.coe_injective
gramSchmidt_ne_zero_coe 📖	—	LinearIndependent Set Set.instMembership Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 toNormedSpace	—	—	span_gramSchmidt_Iio Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton gramSchmidt_def' zero_add Submodule.sum_mem Submodule.starProjection_singleton Submodule.smul_mem Submodule.subset_span Finset.mem_Iio le_refl Set.image_comp Set.image_subtype_val_Iic_Iio LinearIndependent.notMem_span_image IsLocalRing.toNontrivial Field.instIsLocalRing
gramSchmidt_of_orthogonal 📖	mathematical	Pairwise Inner.inner toInner NormedAddCommGroup.toSeminormedAddCommGroup MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	gramSchmidt	—	Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton gramSchmidt_def Finset.sum_eq_zero Submodule.starProjection_apply Submodule.coe_eq_zero Submodule.isOrtho_span LT.lt.ne lt_of_le_of_lt Finset.mem_Iio Submodule.orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero Submodule.mem_orthogonal_singleton_iff_inner_left Submodule.mem_orthogonal_singleton_iff_inner_right gramSchmidt_mem_span le_refl sub_zero
gramSchmidt_orthogonal 📖	mathematical	—	Inner.inner toInner NormedAddCommGroup.toSeminormedAddCommGroup gramSchmidt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	wellFounded_lt Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton gramSchmidt_def Finset.sum_congr Submodule.starProjection_singleton inner_sub_right inner_sum inner_smul_right Finset.sum_eq_single_of_mem Finset.mem_Iio NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Ne.lt_or_gt inner_eq_zero_symm inner_zero_left zero_div MulZeroClass.zero_mul sub_zero RCLike.ofReal_pow inner_self_eq_norm_sq_to_K div_mul_cancel₀ inner_self_ne_zero sub_self
gramSchmidt_pairwise_orthogonal 📖	mathematical	—	Pairwise Inner.inner toInner NormedAddCommGroup.toSeminormedAddCommGroup gramSchmidt MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	gramSchmidt_orthogonal
gramSchmidt_triangular 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	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 toNormedSpace Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr gramSchmidt Module.Basis Module.Basis.instFunLike NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing	—	Submodule.subset_span Set.mem_image span_gramSchmidt_Iio RingHomInvPair.ids Module.Basis.repr_support_subset_of_mem_span Finsupp.mem_supported' Finsupp.mem_supported Set.self_notMem_Iio
gramSchmidt_zero 📖	mathematical	—	gramSchmidt Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton gramSchmidt_def Finset.sum_congr map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass Finset.sum_const_zero sub_self
inner_gramSchmidtOrthonormalBasis_eq_zero 📖	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 toNormedSpace Fintype.card gramSchmidtNormed NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	Inner.inner toInner DFunLike.coe OrthonormalBasis OrthonormalBasis.instFunLike gramSchmidtOrthonormalBasis MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing	—	Submodule.mem_orthogonal_singleton_iff_inner_right Submodule.isOrtho_span inner_zero_left gramSchmidtOrthonormalBasis_apply OrthonormalBasis.orthonormal span_gramSchmidtNormed mem_span_gramSchmidt le_rfl
mem_span_gramSchmidt 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	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 toNormedSpace SetLike.instMembership Submodule.setLike Submodule.span Set.image gramSchmidt Set.Iic	—	Submodule.HasOrthogonalProjection.ofCompleteSpace complete_of_proper FiniteDimensional.RCLike.properSpace_submodule FiniteDimensional.span_singleton gramSchmidt_def' Finset.sum_congr Submodule.starProjection_singleton Submodule.add_mem Submodule.subset_span Set.mem_image_of_mem Submodule.sum_mem Submodule.smul_mem LE.le.trans LT.lt.le Finset.mem_Iio
span_gramSchmidt 📖	mathematical	—	Submodule.span 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 toNormedSpace Set.range gramSchmidt	—	Submodule.span_eq_span Set.range_subset_iff Submodule.span_mono Set.image_subset_range gramSchmidt_mem_span le_rfl mem_span_gramSchmidt
span_gramSchmidtNormed 📖	mathematical	—	Submodule.span 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 toNormedSpace Set.image gramSchmidtNormed gramSchmidt	—	Submodule.span_eq_span Set.image_subset_iff Submodule.smul_mem Submodule.subset_span Set.mem_image_of_mem Submodule.span_mono Set.image_mono Finset.singleton_subset_set_iff Finset.coe_singleton Set.image_singleton AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass Submodule.mem_span_singleton smul_inv_smul₀ Nat.cast_zero algebraMap.coe_zero Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing IsLocalRing.toNontrivial Field.instIsLocalRing norm_ne_zero_iff
span_gramSchmidtNormed_range 📖	mathematical	—	Submodule.span 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 toNormedSpace Set.range gramSchmidtNormed gramSchmidt	—	Set.image_univ span_gramSchmidtNormed
span_gramSchmidt_Iic 📖	mathematical	—	Submodule.span 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 toNormedSpace Set.image gramSchmidt Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Submodule.span_eq_span Set.image_subset_iff gramSchmidt_mem_span mem_span_gramSchmidt
span_gramSchmidt_Iio 📖	mathematical	—	Submodule.span 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 toNormedSpace Set.image gramSchmidt Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Submodule.span_eq_span Set.image_subset_iff Submodule.span_mono Set.image_mono Set.Iic_subset_Iio gramSchmidt_mem_span le_rfl mem_span_gramSchmidt

---

← Back to Index