BaseChange

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

Statistics

Metric	Count
Definitions	0
Theorems det_baseChange, charpoly_baseChange, det_baseChange, det_eq_sign_charpoly_coeff	4
Total	4

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_baseChange 📖	mathematical	—	DFunLike.coe MonoidHom LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddCommGroup.toAddCommMonoid Algebra.toModule TensorProduct.addCommGroup Ring.toAddCommGroup CommRing.toRing TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid automorphismGroup Units.instMulOneClass MonoidHom.instFunLike det baseChange Units.map MonoidHomClass.toMonoidHom RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass NonAssocSemiring.toMulZeroOneClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass algebraMap	—	RingHomInvPair.ids Units.ext Algebra.to_smulCommClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass LinearMap.det_baseChange

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charpoly_baseChange 📖	mathematical	—	charpoly TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring AddCommGroup.toAddCommMonoid Algebra.toModule TensorProduct.addCommGroup Ring.toAddCommGroup CommRing.toRing TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Module.Free.tensor IsScalarTower.right Module.Free.self Module.Finite.base_change baseChange Polynomial.map algebraMap	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Algebra.to_smulCommClass Module.Free.tensor IsScalarTower.right Module.Free.self Module.Finite.base_change Unique.instSubsingleton RingHom.domain_nontrivial RingHomInvPair.ids smulCommClass_self Finite.of_fintype charpoly_toMatrix Matrix.charpoly_map Matrix.ext toMatrix_apply Module.Basis.baseChange_apply Module.Basis.baseChange_repr_tmul
det_baseChange 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddCommGroup.toAddCommMonoid Algebra.toModule TensorProduct.addCommGroup Ring.toAddCommGroup CommRing.toRing TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det baseChange RingHom RingHom.instFunLike algebraMap	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Algebra.to_smulCommClass det_eq_one_of_subsingleton Unique.instSubsingleton RingHom.domain_nontrivial Module.Free.tensor IsScalarTower.right Module.Free.self Module.Finite.base_change det_eq_sign_charpoly_coeff IsScalarTower.to_smulCommClass Module.finrank_tensorProduct commRing_strongRankCondition Module.finrank_self one_mul charpoly_baseChange Polynomial.coeff_map map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_neg RingHomClass.toAddMonoidHomClass map_one MonoidHomClass.toOneHomClass
det_eq_sign_charpoly_coeff 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Module.finrank Polynomial.coeff charpoly	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Module.finrank_subsingleton pow_one neg_mul one_mul RingHomInvPair.ids smulCommClass_self Finite.of_fintype det_toMatrix Matrix.det_eq_sign_charpoly_coeff Module.finrank_eq_card_chooseBasisIndex commRing_strongRankCondition charpoly_def

---

← Back to Index