ToMatrix

📁 Source: Mathlib/LinearAlgebra/Charpoly/ToMatrix.lean

Statistics

Metric	Count
Definitions	0
Theorems charpoly_conj, charpoly_prodMap, charpoly_toMatrix, charpoly_mulVecLin, charpoly_toLin, charpoly_toLin'	6
Total	6

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charpoly_conj 📖	mathematical	—	LinearMap.charpoly DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Module.End AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv conj	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype LinearMap.charpoly_toMatrix Matrix.ext RingHomCompTriple.ids Module.Basis.equivFun_symm_apply Fintype.sum_single_smul one_smul symm_apply_apply

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charpoly_prodMap 📖	mathematical	—	charpoly Prod.instAddCommGroup Prod.instModule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Module.Free.prod Module.Finite.prod prodMap Polynomial Polynomial.instMul	—	Module.Free.prod Module.Finite.prod RingHomInvPair.ids smulCommClass_self Finite.of_fintype charpoly_toMatrix Finite.instSum toMatrix_prodMap Matrix.charpoly_fromBlocks_zero₁₂
charpoly_toMatrix 📖	mathematical	—	Matrix.charpoly DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap AddCommGroup.toAddCommMonoid Matrix 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 charpoly	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim RingHomInvPair.ids smulCommClass_self Finite.of_fintype Unique.instSubsingleton basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix invariantBasisNumber_of_nontrivial_of_commRing Matrix.charpoly_reindex Matrix.reindexLinearEquiv_mul Matrix.charpoly_mul_comm mul_assoc Matrix.charpoly.congr_simp Matrix.submatrix_mul_equiv Module.Basis.toMatrix_mul_toMatrix Module.Basis.toMatrix_self Matrix.submatrix_id_id Matrix.reindexLinearEquiv_refl_refl one_mul

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charpoly_mulVecLin 📖	mathematical	—	LinearMap.charpoly Pi.addCommGroup Ring.toAddCommGroup CommRing.toRing Pi.Function.module CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Module.Free.function NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring Finite.of_fintype Module.Free.self Module.Finite.pi NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.Finite.self mulVecLin charpoly	—	charpoly_toLin'
charpoly_toLin 📖	mathematical	—	LinearMap.charpoly DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Matrix LinearMap AddCommGroup.toAddCommMonoid 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 charpoly	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype LinearMap.charpoly_toMatrix charpoly.congr_simp LinearMap.toMatrix_toLin
charpoly_toLin' 📖	mathematical	—	LinearMap.charpoly Pi.addCommGroup Ring.toAddCommGroup CommRing.toRing Pi.Function.module CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Module.Free.function NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring Finite.of_fintype Module.Free.self Module.Finite.pi NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.Finite.self DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Matrix LinearMap Pi.addCommMonoid addCommMonoid LinearMap.addCommMonoid module LinearMap.module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin' charpoly	—	Module.Free.function Finite.of_fintype Module.Free.self Module.Finite.pi Module.Finite.self RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass smulCommClass_self toLin_eq_toLin' charpoly_toLin

---

← Back to Index