Minpoly

📁 Source: Mathlib/LinearAlgebra/Matrix/Charpoly/Minpoly.lean

Statistics

Metric	Count
Definitions	0
Theorems minpoly_toMatrix, minpoly_toMatrix', isIntegral, minpoly_dvd_charpoly, minpoly_toLin, minpoly_toLin', charpoly_leftMulMatrix	7
Total	7

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
minpoly_toMatrix 📖	mathematical	—	minpoly Matrix Matrix.instRing CommRing.toRing Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap AddCommGroup.toAddCommMonoid addCommMonoid Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix Finite.of_fintype Module.End.instRing Module.End.instAlgebra CommRing.toCommMonoid Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	minpoly.algEquiv_eq smulCommClass_self IsScalarTower.left
minpoly_toMatrix' 📖	mathematical	—	minpoly Matrix Matrix.instRing CommRing.toRing Matrix.instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule addCommMonoid Matrix.addCommMonoid module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix' NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.End.instRing Pi.addCommGroup Ring.toAddCommGroup Module.End.instAlgebra Algebra.toSMul Pi.isScalarTower IsScalarTower.right	—	minpoly.algEquiv_eq Function.smulCommClass Algebra.to_smulCommClass Pi.isScalarTower IsScalarTower.right

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIntegral 📖	mathematical	—	IsIntegral Matrix instRing CommRing.toRing instAlgebra CommRing.toCommSemiring Ring.toSemiring Algebra.id	—	charpoly_monic aeval_self_charpoly
minpoly_dvd_charpoly 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing minpoly Matrix instRing DivisionRing.toRing Field.toDivisionRing instAlgebra Ring.toSemiring Algebra.id charpoly	—	minpoly.dvd aeval_self_charpoly
minpoly_toLin 📖	mathematical	—	minpoly LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Module.End.instRing Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.addCommMonoid module Semiring.toModule LinearMap.module CommSemiring.toCommMonoid EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin Finite.of_fintype instRing instAlgebra	—	minpoly.algEquiv_eq smulCommClass_self IsScalarTower.left
minpoly_toLin' 📖	mathematical	—	minpoly LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Module.End.instRing Pi.addCommGroup Ring.toAddCommGroup CommRing.toRing Module.End.instAlgebra Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Algebra.toSMul Pi.isScalarTower IsScalarTower.right DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix addCommMonoid LinearMap.addCommMonoid module LinearMap.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin' instRing instAlgebra Ring.toSemiring	—	minpoly.algEquiv_eq Function.smulCommClass Algebra.to_smulCommClass Pi.isScalarTower IsScalarTower.right

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charpoly_leftMulMatrix 📖	mathematical	—	Matrix.charpoly PowerBasis.dim Fin.fintype DFunLike.coe AlgHom Matrix CommRing.toCommSemiring Ring.toSemiring Matrix.semiring CommSemiring.toSemiring Matrix.instAlgebra Algebra.id AlgHom.funLike Algebra.leftMulMatrix PowerBasis.basis PowerBasis.gen minpoly	—	subsingleton_or_nontrivial Unique.instSubsingleton minpoly.unique' Matrix.charpoly_monic injective_iff_map_eq_zero DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Algebra.leftMulMatrix_injective Polynomial.aeval_algHom_apply Matrix.aeval_self_charpoly Mathlib.Tactic.Contrapose.contrapose₃ PowerBasis.dim_le_degree_of_root Fintype.card_fin Matrix.charpoly_degree_eq_dim

---

← Back to Index