Star

📁 Source: Mathlib/LinearAlgebra/SesquilinearForm/Star.lean

Statistics

Metric	Count
Definitions	0
Theorems isPosSemidef_iff_posSemidef_toMatrix, isSymm_iff_basis, isSymm_iff_isHermitian_toMatrix, apply_eq_star_dotProduct_toMatrix₂_mulVec, star_dotProduct_toMatrix₂_mulVec	5
Total	5

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isPosSemidef_iff_posSemidef_toMatrix 📖	mathematical	—	IsPosSemidef CommRing.toCommSemiring starRingEnd Preorder.toLE PartialOrder.toPreorder Matrix.PosSemidef CommRing.toRing DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂	—	Algebra.to_smulCommClass RingHomInvPair.ids smulCommClass_self instSMulCommClass isPosSemidef_def Matrix.posSemidef_iff_dotProduct_mulVec isSymm_iff_isHermitian_toMatrix isNonneg_def Finite.of_fintype star_dotProduct_toMatrix₂_mulVec apply_eq_star_dotProduct_toMatrix₂_mulVec
isSymm_iff_basis 📖	mathematical	—	IsSymm starRingEnd Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring StarRing.toStarAddMonoid DFunLike.coe LinearMap RingHom.id Semiring.toModule instFunLike addCommMonoid module Algebra.to_smulCommClass Algebra.id Module.Basis Module.Basis.instFunLike	—	Algebra.to_smulCommClass IsSymm.eq Submodule.mem_span_iff_exists_finset_subset Module.Basis.span_eq map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass Finset.sum_congr map_smulₛₗ map_smul SemilinearMapClass.toMulActionSemiHomClass coe_sum Finset.sum_apply Finset.mul_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass star_star Finset.sum_comm mul_left_comm
isSymm_iff_isHermitian_toMatrix 📖	mathematical	—	IsSymm starRingEnd Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring StarRing.toStarAddMonoid DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids LinearMap Semiring.toModule addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Module.toDistribMulAction Matrix Matrix.addCommMonoid instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix₂	—	Algebra.to_smulCommClass RingHomInvPair.ids smulCommClass_self instSMulCommClass isSymm_iff_basis Matrix.IsHermitian.ext_iff toMatrix₂_apply

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_star_dotProduct_toMatrix₂_mulVec 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instFunLike starRingEnd LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Star.star Pi.instStarForall InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Finsupp.instFunLike LinearEquiv RingHomInvPair.ids Finsupp.instAddCommMonoid Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr Matrix.mulVec smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Module.toDistribMulAction Matrix Matrix.addCommMonoid LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module LinearMap.toMatrix₂	—	Algebra.to_smulCommClass apply_eq_dotProduct_toMatrix₂_mulVec
star_dotProduct_toMatrix₂_mulVec 📖	mathematical	—	dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Star.star Pi.instStarForall InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid Matrix.mulVec DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids LinearMap starRingEnd Semiring.toModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Module.toDistribMulAction Matrix Matrix.addCommMonoid LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix₂ LinearMap.instFunLike Algebra.to_smulCommClass Algebra.id Pi.addCommMonoid Pi.Function.module LinearEquiv.symm Module.Basis.equivFun Finite.of_fintype	—	Algebra.to_smulCommClass dotProduct_toMatrix₂_mulVec

---

← Back to Index