GramMatrix

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

Statistics

Metric	Count
Definitions gram	1
Theorems gram_apply, gram_single, gram_zero, isHermitian_gram, linearIndependent_of_posDef_gram, posDef_gram_iff_linearIndependent, posDef_gram_of_linearIndependent, posSemidef_gram, star_dotProduct_gram_mulVec, submatrix_gram	10
Total	11

Matrix

Definitions

Name	Category	Theorems
gram 📖	CompOp	9 math math: gram_zero, posDef_gram_of_linearIndependent, posDef_gram_iff_linearIndependent, isHermitian_gram, posSemidef_gram, star_dotProduct_gram_mulVec, submatrix_gram, gram_apply, gram_single

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gram_apply 📖	mathematical	—	gram Inner.inner	—	—
gram_single 📖	mathematical	—	gram InnerProductSpace.toInner Pi.single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField Inner.inner	—	ext ne_or_eq Pi.single_eq_of_ne' inner_zero_left single.congr_simp inner_self_eq_norm_sq_to_K single_apply_of_ne Pi.single_eq_same inner_zero_right single_apply_same
gram_zero 📖	mathematical	—	gram InnerProductSpace.toInner Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Matrix zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	ext inner_zero_left
isHermitian_gram 📖	mathematical	—	IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing gram InnerProductSpace.toInner	—	ext inner_conj_symm
linearIndependent_of_posDef_gram 📖	mathematical	PosDef NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.toPartialOrder RCLike.toStarRing gram InnerProductSpace.toInner	LinearIndependent DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace	—	Fintype.linearIndependent_iff PosDef.dotProduct_mulVec_pos star_dotProduct_gram_mulVec inner_self_eq_norm_sq_to_K norm_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat
posDef_gram_iff_linearIndependent 📖	mathematical	—	PosDef NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.toPartialOrder RCLike.toStarRing gram InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup LinearIndependent DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace	—	linearIndependent_of_posDef_gram posDef_gram_of_linearIndependent
posDef_gram_of_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 InnerProductSpace.toNormedSpace	PosDef NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing RCLike.toPartialOrder RCLike.toStarRing gram InnerProductSpace.toInner	—	PosDef.of_dotProduct_mulVec_pos isHermitian_gram LE.le.lt_of_ne' PosSemidef.dotProduct_mulVec_nonneg posSemidef_gram star_dotProduct_gram_mulVec Iff.ne inner_self_eq_zero Fintype.linearIndependent_iff
posSemidef_gram 📖	mathematical	—	PosSemidef NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.toPartialOrder RCLike.toStarRing gram InnerProductSpace.toInner	—	PosSemidef.of_dotProduct_mulVec_nonneg isHermitian_gram star_dotProduct_gram_mulVec RCLike.le_iff_re_im map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass inner_self_eq_norm_sq_to_K RCLike.re_ofReal_pow IsOrderedRing.toPosMulMono Real.instIsOrderedRing RCLike.im_ofReal_pow
star_dotProduct_gram_mulVec 📖	mathematical	—	dotProduct 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 Star.star Pi.instStarForall InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid RCLike.toStarRing mulVec gram InnerProductSpace.toInner Inner.inner 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 Module.toDistribMulAction NormedSpace.toModule InnerProductSpace.toNormedSpace	—	Finset.sum_congr mul_assoc mul_comm sum_inner inner_sum inner_smul_left inner_smul_right
submatrix_gram 📖	mathematical	—	submatrix Set.Elem gram InnerProductSpace.toInner	—	—

---

← Back to Index