Hermitian

📁 Source: Mathlib/Analysis/Matrix/Hermitian.lean

Statistics

Metric	Count
Definitions	0
Theorems isHermitian_toMatrix_iff, coe_re_apply_self, coe_re_diag, im_star_dotProduct_mulVec_self, isHermitian_iff_isSymmetric, isSymmetric_toEuclideanLin_iff, isSymmetric_toLin_iff	7
Total	7

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isHermitian_toMatrix_iff 📖	mathematical	—	Matrix.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 DFunLike.coe LinearEquiv CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Matrix addCommMonoid Matrix.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Finite.of_fintype OrthonormalBasis.toBasis IsSymmetric	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype Matrix.isSymmetric_toLin_iff Matrix.toLin_toMatrix

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isHermitian_iff_isSymmetric 📖	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 LinearMap.IsSymmetric EuclideanSpace PiLp.seminormedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing PiLp.innerProductSpace NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing RCLike.innerProductSpace DFunLike.coe LinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap ESeminormedAddCommMonoid.toAddCommMonoid PiLp.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid PiLp.normedAddCommGroup AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup Pi.addCommGroup NormedAddCommGroup.toAddCommGroup WithLp.instModule SeminormedAddCommGroup.toAddCommGroup Pi.Function.module NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedSpace.toModule InnerProductSpace.toNormedSpace 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 Algebra.to_smulCommClass Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toEuclideanLin	—	fact_one_le_two_ennreal RingHomInvPair.ids WithLp.instSMulCommClass Function.smulCommClass Algebra.to_smulCommClass isSymmetric_toEuclideanLin_iff
isSymmetric_toEuclideanLin_iff 📖	mathematical	—	LinearMap.IsSymmetric 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 DFunLike.coe LinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap ESeminormedAddCommMonoid.toAddCommMonoid PiLp.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid PiLp.normedAddCommGroup 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 InnerProductSpace.toNormedSpace 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 IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing StarRing.toStarAddMonoid RCLike.toStarRing	—	isSymmetric_toLin_iff fact_one_le_two_ennreal
isSymmetric_toLin_iff 📖	mathematical	—	LinearMap.IsSymmetric NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearEquiv CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid module Semiring.toModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin Finite.of_fintype OrthonormalBasis.toBasis IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing StarRing.toStarAddMonoid RCLike.toStarRing	—	Module.Basis.finiteDimensional_of_finite Finite.of_fintype RingHomInvPair.ids smulCommClass_self RingHomInvPair.instStarRingEnd EquivLike.toEmbeddingLike LinearMap.ext ext_inner_right IsHermitian.eq

Matrix.IsHermitian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_re_apply_self 📖	mathematical	Matrix.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	RCLike.ofReal DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re	—	RCLike.conj_eq_iff_re RCLike.star_def Matrix.conjTranspose_apply eq
coe_re_diag 📖	mathematical	Matrix.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	RCLike.ofReal DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Matrix.diag	—	coe_re_apply_self
im_star_dotProduct_mulVec_self 📖	mathematical	Matrix.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	DFunLike.coe AddMonoidHom Real AddMonoid.toZero AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.im dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib 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 Star.star Pi.instStarForall InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid RCLike.toStarRing Matrix.mulVec Real.instZero	—	dotProduct_comm LinearMap.IsSymmetric.im_inner_self_apply fact_one_le_two_ennreal RingHomInvPair.ids WithLp.instSMulCommClass Function.smulCommClass Algebra.to_smulCommClass Matrix.isSymmetric_toEuclideanLin_iff

---

← Back to Index