Hermitian

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

Statistics

Metric	Count
Definitions	0
Theorems coe_re_apply_self, coe_re_diag, im_star_dotProduct_mulVec_self, isHermitian_iff_isSymmetric	4
Total	4

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 LinearMap.IsSymmetric.eq_1 Function.Surjective.forall₂ WithLp.toLp_surjective star_mulVec dotProduct_comm dotProduct_mulVec ext Pi.single_star star_one single_vecMul one_smul single_dotProduct one_mul mulVec_single dotProduct_single mul_one

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 NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField 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 NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField 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 NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.im dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Star.star Pi.instStarForall 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.isHermitian_iff_isSymmetric

---

← Back to Index