Polynomial

📁 Source: Mathlib/Algebra/Module/LinearMap/Polynomial.lean

Statistics

Metric	Count
Definitions `IsNilRegular`, `nilRank`, `nilRankAux`, `polyCharpoly`, `polyCharpolyAux`, `toMvPolynomial`, `toMvPolynomial`	7
Theorems `exists_isNilRegular`, `exists_isNilRegular_of_finrank_le_card`, `isNilRegular_def`, `isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero`, `isNilRegular_iff_natTrailingDegree_charpoly_eq_nilRank`, `nilRankAux_basis_indep`, `nilRankAux_le`, `nilRank_eq_polyCharpoly_natTrailingDegree`, `nilRank_le_card`, `nilRank_le_finrank`, `nilRank_le_natTrailingDegree_charpoly`, `polyCharpolyAux_baseChange`, `polyCharpolyAux_basisIndep`, `polyCharpolyAux_coeff_eval`, `polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff`, `polyCharpolyAux_map_aeval`, `polyCharpolyAux_map_eq_charpoly`, `polyCharpolyAux_map_eq_toMatrix_charpoly`, `polyCharpolyAux_map_eval`, `polyCharpoly_baseChange`, `polyCharpoly_coeff_eq_zero_iff_of_basis`, `polyCharpoly_coeff_eq_zero_of_basis`, `polyCharpoly_coeff_eval`, `polyCharpoly_coeff_isHomogeneous`, `polyCharpoly_coeff_nilRankAux_ne_zero`, `polyCharpoly_coeff_nilRank_ne_zero`, `polyCharpoly_eq_of_basis`, `polyCharpoly_map_eq_charpoly`, `polyCharpoly_monic`, `polyCharpoly_natDegree`, `polyCharpoly_ne_zero`, `toMvPolynomial_add`, `toMvPolynomial_baseChange`, `toMvPolynomial_comp`, `toMvPolynomial_constantCoeff`, `toMvPolynomial_eval_eq_apply`, `toMvPolynomial_id`, `toMvPolynomial_isHomogeneous`, `toMvPolynomial_totalDegree_le`, `toMvPolynomial_zero`, `toMvPolynomial_add`, `toMvPolynomial_constantCoeff`, `toMvPolynomial_eval_eq_apply`, `toMvPolynomial_isHomogeneous`, `toMvPolynomial_map`, `toMvPolynomial_mul`, `toMvPolynomial_one`, `toMvPolynomial_totalDegree_le`, `toMvPolynomial_zero`	49
Total	56

LinearMap

Definitions

Name	Category	Theorems
`IsNilRegular` 📖	MathDef	5 math math: `isNilRegular_iff_natTrailingDegree_charpoly_eq_nilRank`, `exists_isNilRegular`, `isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero`, `exists_isNilRegular_of_finrank_le_card`, `isNilRegular_def`
`nilRank` 📖	CompOp	5 math math: `isNilRegular_iff_natTrailingDegree_charpoly_eq_nilRank`, `nilRank_eq_polyCharpoly_natTrailingDegree`, `nilRank_le_card`, `nilRank_le_natTrailingDegree_charpoly`, `nilRank_le_finrank`
`nilRankAux` 📖	CompOp	2 math math: `nilRankAux_basis_indep`, `nilRankAux_le`
`polyCharpoly` 📖	CompOp	12 math math: `nilRankAux_basis_indep`, `polyCharpoly_coeff_isHomogeneous`, `nilRank_eq_polyCharpoly_natTrailingDegree`, `polyCharpoly_baseChange`, `LieModule.rank_eq_natTrailingDegree`, `polyCharpoly_eq_of_basis`, `polyCharpoly_map_eq_charpoly`, `polyCharpoly_monic`, `LieAlgebra.rank_eq_natTrailingDegree`, `polyCharpoly_coeff_eq_zero_iff_of_basis`, `polyCharpoly_natDegree`, `polyCharpoly_coeff_eval`
`polyCharpolyAux` 📖	CompOp	8 math math: `polyCharpolyAux_map_eval`, `polyCharpolyAux_map_eq_charpoly`, `polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff`, `polyCharpolyAux_basisIndep`, `polyCharpolyAux_baseChange`, `polyCharpolyAux_map_aeval`, `polyCharpolyAux_coeff_eval`, `polyCharpolyAux_map_eq_toMatrix_charpoly`
`toMvPolynomial` 📖	CompOp	10 math math: `toMvPolynomial_totalDegree_le`, `toMvPolynomial_add`, `toMvPolynomial_zero`, `toMvPolynomial_baseChange`, `polyCharpoly_eq_of_basis`, `toMvPolynomial_constantCoeff`, `toMvPolynomial_comp`, `toMvPolynomial_isHomogeneous`, `toMvPolynomial_eval_eq_apply`, `toMvPolynomial_id`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isNilRegular` 📖	mathematical	—	`IsNilRegular`	—	`smulCommClass_self` `exists_isNilRegular_of_finrank_le_card` `LE.le.trans` `Cardinal.natCast_le_aleph0` `Cardinal.infinite_iff`
`exists_isNilRegular_of_finrank_le_card` 📖	mathematical	—	`IsNilRegular`	—	`smulCommClass_self` `polyCharpoly_coeff_isHomogeneous` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `nilRank_le_card` `IsDomain.toNontrivial` `Module.finrank_eq_card_chooseBasisIndex` `commRing_strongRankCondition` `polyCharpoly_coeff_nilRank_ne_zero` `MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero_of_le_card` `le_trans` `Cardinal.addLeftMono` `IsOrderedRing.toZeroLEOneClass` `Cardinal.isOrderedRing` `Cardinal.instCharZero` `Finite.of_fintype` `RingHomInvPair.ids` `isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero` `LinearEquiv.apply_symm_apply`
`isNilRegular_def` 📖	mathematical	—	`IsNilRegular`	—	`smulCommClass_self`
`isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero` 📖	mathematical	—	`IsNilRegular`	—	`smulCommClass_self` `RingHomInvPair.ids` `IsNilRegular.eq_1` `polyCharpoly_coeff_eval`
`isNilRegular_iff_natTrailingDegree_charpoly_eq_nilRank` 📖	mathematical	—	`IsNilRegular` `Polynomial.natTrailingDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `charpoly` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.End` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `instFunLike` `nilRank`	—	`smulCommClass_self` `isNilRegular_def` `le_antisymm` `Polynomial.natTrailingDegree_le_of_ne_zero` `nilRank_le_natTrailingDegree_charpoly` `Polynomial.trailingCoeff_nonzero_iff_nonzero` `Polynomial.Monic.ne_zero` `charpoly_monic`
`nilRankAux_basis_indep` 📖	mathematical	—	`nilRankAux` `Polynomial.natTrailingDegree` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `polyCharpoly`	—	`smulCommClass_self` `le_antisymm` `nilRankAux_le`
`nilRankAux_le` 📖	mathematical	—	`nilRankAux`	—	`smulCommClass_self` `Polynomial.natTrailingDegree_le_of_ne_zero` `Iff.not` `polyCharpoly_coeff_eq_zero_iff_of_basis` `polyCharpoly_coeff_nilRankAux_ne_zero`
`nilRank_eq_polyCharpoly_natTrailingDegree` 📖	mathematical	—	`nilRank` `Polynomial.natTrailingDegree` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `polyCharpoly`	—	`smulCommClass_self` `nilRankAux_basis_indep`
`nilRank_le_card` 📖	mathematical	—	`nilRank` `Fintype.card`	—	`smulCommClass_self` `Polynomial.natTrailingDegree_le_of_ne_zero` `Module.finrank_eq_card_basis` `commRing_strongRankCondition` `polyCharpoly_natDegree` `Polynomial.coeff_natDegree` `Polynomial.Monic.leadingCoeff` `polyCharpoly_monic` `one_ne_zero` `NeZero.one` `MvPolynomial.nontrivial_of_nontrivial`
`nilRank_le_finrank` 📖	mathematical	—	`nilRank` `Module.finrank` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`smulCommClass_self` `Module.finrank_eq_card_chooseBasisIndex` `commRing_strongRankCondition` `nilRank_le_card`
`nilRank_le_natTrailingDegree_charpoly` 📖	mathematical	—	`nilRank` `Polynomial.natTrailingDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `charpoly` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.End` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `instFunLike`	—	`smulCommClass_self` `Polynomial.natTrailingDegree_le_of_ne_zero` `Polynomial.trailingCoeff_nonzero_iff_nonzero` `Polynomial.Monic.ne_zero` `charpoly_monic` `RingHomInvPair.ids` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `polyCharpoly_coeff_eval`
`polyCharpolyAux_baseChange` 📖	mathematical	—	`polyCharpolyAux` `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` `comp` `Module.End` `addCommMonoid` `RingHom.id` `module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `TensorProduct.addCommMonoid` `RingHomCompTriple.ids` `tensorProduct` `baseChange` `Algebra.TensorProduct.basis` `Polynomial.map` `MvPolynomial` `MvPolynomial.commSemiring` `MvPolynomial.map` `algebraMap`	—	`smulCommClass_self` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `Matrix.charpoly.univ_map_map` `Polynomial.map_map` `MvPolynomial.ringHom_ext` `MvPolynomial.map_C` `MvPolynomial.bind₁_C_right` `MvPolynomial.map_X` `MvPolynomial.bind₁_X_right` `Finite.of_fintype` `toMvPolynomial_comp` `toMvPolynomial_baseChange` `Finite.instProd` `RingHomInvPair.ids` `toMatrix_apply` `TensorProduct.smulCommClass_left` `tensorProduct.eq_1` `IsScalarTower.to_smulCommClass` `IsScalarTower.compatibleSMul` `instIsScalarTower` `TensorProduct.AlgebraTensorModule.lift_apply` `Algebra.TensorProduct.basis_apply` `TensorProduct.lift.tmul` `coe_restrictScalars` `one_smul` `Module.Basis.baseChange_end` `Module.Basis.repr_self_apply` `Finset.sum_eq_single` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass` `MvPolynomial.X.eq_1`
`polyCharpolyAux_basisIndep` 📖	mathematical	—	`polyCharpolyAux`	—	`smulCommClass_self` `MvPolynomial.aeval_X_left` `Polynomial.map_injective` `Algebra.to_smulCommClass` `Module.Finite.of_basis` `Finite.of_fintype` `Module.Free.of_basis` `TensorProduct.smulCommClass_left` `RingHomCompTriple.ids` `RingHomInvPair.ids` `polyCharpolyAux_map_aeval`
`polyCharpolyAux_coeff_eval` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.eval` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `Polynomial.coeff` `polyCharpolyAux` `charpoly` `LinearMap` `Module.End` `addCommMonoid` `module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `instFunLike`	—	`smulCommClass_self` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `RingHomInvPair.ids` `polyCharpolyAux_map_eq_charpoly` `Polynomial.coeff_map`
`polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.eval` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `Polynomial.coeff` `polyCharpolyAux` `Matrix.charpoly` `LinearMap` `Matrix` `addCommMonoid` `Matrix.addCommMonoid` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Matrix.module` `toMatrix` `Finite.of_fintype` `Module.End` `CommRing.toCommMonoid` `Ring.toSemiring` `CommRing.toRing` `instFunLike`	—	`smulCommClass_self` `RingHomInvPair.ids` `Finite.of_fintype` `polyCharpolyAux_map_eq_toMatrix_charpoly` `Polynomial.coeff_map`
`polyCharpolyAux_map_aeval` 📖	mathematical	—	`Polynomial.map` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `AlgHom.toRingHom` `MvPolynomial.algebra` `Algebra.id` `MvPolynomial.aeval` `polyCharpolyAux` `charpoly` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Algebra.toModule` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `TensorProduct.leftModule` `Semiring.toModule` `Algebra.to_smulCommClass` `DFunLike.coe` `LinearMap` `RingHom.id` `TensorProduct.addCommMonoid` `addCommMonoid` `module` `TensorProduct.smulCommClass_left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `instFunLike` `comp` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `RingHomCompTriple.ids` `tensorProduct` `baseChange` `LinearEquiv` `RingHomInvPair.ids` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Finsupp.instAddCommMonoid` `Finsupp.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `Module.Basis.repr` `Algebra.TensorProduct.basis` `Equiv` `Equiv.instEquivLike` `Equiv.symm` `Finsupp.equivFunOnFinite` `Finite.of_fintype`	—	`smulCommClass_self` `Algebra.to_smulCommClass` `TensorProduct.smulCommClass_left` `RingHomCompTriple.ids` `RingHomInvPair.ids` `Finite.of_fintype` `polyCharpolyAux_map_eval` `polyCharpolyAux_baseChange` `Polynomial.map_map` `DFunLike.ext` `MvPolynomial.eval_map`
`polyCharpolyAux_map_eq_charpoly` 📖	mathematical	—	`Polynomial.map` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.eval` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `polyCharpolyAux` `charpoly` `LinearMap` `Module.End` `addCommMonoid` `module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `instFunLike`	—	`smulCommClass_self` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `RingHomInvPair.ids` `Unique.instSubsingleton` `Finite.of_fintype` `polyCharpolyAux_map_eq_toMatrix_charpoly` `charpoly_toMatrix`
`polyCharpolyAux_map_eq_toMatrix_charpoly` 📖	mathematical	—	`Polynomial.map` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.eval` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `polyCharpolyAux` `Matrix.charpoly` `LinearMap` `Matrix` `addCommMonoid` `Matrix.addCommMonoid` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Matrix.module` `toMatrix` `Finite.of_fintype` `Module.End` `CommRing.toCommMonoid` `Ring.toSemiring` `CommRing.toRing` `instFunLike`	—	`smulCommClass_self` `RingHomInvPair.ids` `Finite.of_fintype` `polyCharpolyAux.eq_1` `Polynomial.map_map` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `MvPolynomial.eval₂Hom_C_eq_bind₁` `MvPolynomial.comp_eval₂Hom` `Matrix.charpoly.univ_map_eval₂Hom` `Matrix.ext` `Matrix.of_apply` `toMvPolynomial_eval_eq_apply` `LinearEquiv.symm_apply_apply`
`polyCharpolyAux_map_eval` 📖	mathematical	—	`Polynomial.map` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.eval` `polyCharpolyAux` `charpoly` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.End` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `instFunLike` `LinearEquiv` `RingHomInvPair.ids` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `Module.Basis.repr` `Equiv` `Equiv.instEquivLike` `Equiv.symm` `Finsupp.equivFunOnFinite` `Finite.of_fintype`	—	`smulCommClass_self` `RingHomInvPair.ids` `Finite.of_fintype` `polyCharpolyAux_map_eq_charpoly` `LinearEquiv.apply_symm_apply`
`polyCharpoly_baseChange` 📖	mathematical	—	`polyCharpoly` `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` `comp` `Module.End` `addCommMonoid` `RingHom.id` `module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `TensorProduct.addCommMonoid` `RingHomCompTriple.ids` `tensorProduct` `baseChange` `Algebra.TensorProduct.instFree` `Module.Finite.base_change` `Algebra.TensorProduct.basis` `Polynomial.map` `MvPolynomial` `MvPolynomial.commSemiring` `MvPolynomial.map` `algebraMap`	—	`smulCommClass_self` `Algebra.to_smulCommClass` `RingHomCompTriple.ids` `Algebra.TensorProduct.instFree` `Module.Finite.base_change` `polyCharpolyAux_baseChange` `polyCharpolyAux_basisIndep`
`polyCharpoly_coeff_eq_zero_iff_of_basis` 📖	mathematical	—	`Polynomial.coeff` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `polyCharpoly` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial`	—	`smulCommClass_self` `polyCharpoly_coeff_eq_zero_of_basis`
`polyCharpoly_coeff_eq_zero_of_basis` 📖	—	`Polynomial.coeff` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `polyCharpoly` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial`	—	—	`smulCommClass_self` `polyCharpoly.eq_1` `polyCharpolyAux.eq_1` `Polynomial.coeff_map` `Finite.of_fintype` `Finite.instProd` `toMvPolynomial_comp` `MvPolynomial.bind₁_bind₁` `RingHom.coe_coe` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`
`polyCharpoly_coeff_eval` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.eval` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `Polynomial.coeff` `polyCharpoly` `charpoly` `LinearMap` `Module.End` `addCommMonoid` `module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `instFunLike`	—	`smulCommClass_self` `RingHomInvPair.ids` `polyCharpoly.eq_1` `polyCharpolyAux_coeff_eval`
`polyCharpoly_coeff_isHomogeneous` 📖	mathematical	`Module.finrank` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	`MvPolynomial.IsHomogeneous` `Polynomial.coeff` `MvPolynomial` `MvPolynomial.commSemiring` `polyCharpoly`	—	`smulCommClass_self` `polyCharpoly.eq_1` `polyCharpolyAux.eq_1` `Polynomial.coeff_map` `one_mul` `MvPolynomial.IsHomogeneous.eval₂` `Matrix.charpoly.univ_coeff_isHomogeneous` `Module.finrank_eq_card_chooseBasisIndex` `commRing_strongRankCondition` `MvPolynomial.isHomogeneous_C` `toMvPolynomial_isHomogeneous`
`polyCharpoly_coeff_nilRankAux_ne_zero` 📖	—	—	—	—	`smulCommClass_self` `Polynomial.trailingCoeff_nonzero_iff_nonzero` `polyCharpoly_ne_zero`
`polyCharpoly_coeff_nilRank_ne_zero` 📖	—	—	—	—	`smulCommClass_self` `nilRank_eq_polyCharpoly_natTrailingDegree` `polyCharpoly_coeff_nilRankAux_ne_zero`
`polyCharpoly_eq_of_basis` 📖	mathematical	—	`polyCharpoly` `Polynomial.map` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHomClass.toRingHom` `AlgHom` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `Semiring.toNonAssocSemiring` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `MvPolynomial.bind₁` `toMvPolynomial` `Module.End` `AddCommGroup.toAddCommMonoid` `addCommGroup` `RingHom.id` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Finite.instProd` `Finite.of_fintype` `Module.Basis.end` `Matrix.charpoly.univ`	—	`smulCommClass_self` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Finite.instProd` `Finite.of_fintype` `polyCharpoly.eq_1` `polyCharpolyAux_basisIndep` `polyCharpolyAux.eq_1`
`polyCharpoly_map_eq_charpoly` 📖	mathematical	—	`Polynomial.map` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `MvPolynomial.eval` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `polyCharpoly` `charpoly` `LinearMap` `Module.End` `addCommMonoid` `module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `instFunLike`	—	`smulCommClass_self` `RingHomInvPair.ids` `polyCharpoly.eq_1` `polyCharpolyAux_map_eq_charpoly`
`polyCharpoly_monic` 📖	mathematical	—	`Polynomial.Monic` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `polyCharpoly`	—	`smulCommClass_self` `Polynomial.Monic.map` `Matrix.charpoly.univ_monic`
`polyCharpoly_natDegree` 📖	mathematical	—	`Polynomial.natDegree` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `polyCharpoly` `Module.finrank` `AddCommGroup.toAddCommMonoid`	—	`smulCommClass_self` `polyCharpoly.eq_1` `polyCharpolyAux.eq_1` `Polynomial.Monic.natDegree_map` `MvPolynomial.nontrivial_of_nontrivial` `Matrix.charpoly.univ_monic` `Matrix.charpoly.univ_natDegree` `Module.finrank_eq_card_chooseBasisIndex` `commRing_strongRankCondition`
`polyCharpoly_ne_zero` 📖	—	—	—	—	`smulCommClass_self` `Polynomial.Monic.ne_zero` `MvPolynomial.nontrivial_of_nontrivial` `polyCharpoly_monic`
`toMvPolynomial_add` 📖	mathematical	—	`toMvPolynomial` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instAdd` `Pi.instAdd` `MvPolynomial` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial`	—	`map_add` `SemilinearMapClass.toAddHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `Matrix.toMvPolynomial_add`
`toMvPolynomial_baseChange` 📖	mathematical	—	`toMvPolynomial` `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` `Algebra.TensorProduct.basis` `baseChange` `DFunLike.coe` `RingHom` `MvPolynomial` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.map` `algebraMap`	—	`Algebra.to_smulCommClass` `RingHomInvPair.ids` `smulCommClass_self` `toMatrix_baseChange` `Matrix.toMvPolynomial_map`
`toMvPolynomial_comp` 📖	mathematical	—	`toMvPolynomial` `comp` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `DFunLike.coe` `AlgHom` `MvPolynomial` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.bind₁` `Finite.of_fintype`	—	`RingHomCompTriple.ids` `Finite.of_fintype` `RingHomInvPair.ids` `smulCommClass_self` `toMatrix_comp` `Matrix.toMvPolynomial_mul`
`toMvPolynomial_constantCoeff` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.constantCoeff` `toMvPolynomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Matrix.toMvPolynomial_constantCoeff`
`toMvPolynomial_eval_eq_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.eval` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finsupp.instFunLike` `toMvPolynomial` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.repr` `LinearMap` `instFunLike` `LinearEquiv.symm`	—	`RingHomInvPair.ids` `toMvPolynomial.eq_1` `Matrix.toMvPolynomial_eval_eq_apply` `smulCommClass_self` `toMatrix_mulVec_repr` `LinearEquiv.apply_symm_apply`
`toMvPolynomial_id` 📖	mathematical	—	`toMvPolynomial` `Finite.of_fintype` `id` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `MvPolynomial.X`	—	`Finite.of_fintype` `toMatrix_id` `Matrix.toMvPolynomial_one`
`toMvPolynomial_isHomogeneous` 📖	mathematical	—	`MvPolynomial.IsHomogeneous` `CommRing.toCommSemiring` `toMvPolynomial`	—	`Matrix.toMvPolynomial_isHomogeneous`
`toMvPolynomial_totalDegree_le` 📖	mathematical	—	`MvPolynomial.totalDegree` `CommRing.toCommSemiring` `toMvPolynomial`	—	`Matrix.toMvPolynomial_totalDegree_le`
`toMvPolynomial_zero` 📖	mathematical	—	`toMvPolynomial` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instZero` `Pi.instZero` `MvPolynomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `MvPolynomial.instCommRingMvPolynomial`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `Matrix.toMvPolynomial_zero`

Matrix

Definitions

Name	Category	Theorems
`toMvPolynomial` 📖	CompOp	9 math math: `toMvPolynomial_add`, `toMvPolynomial_one`, `toMvPolynomial_totalDegree_le`, `toMvPolynomial_map`, `toMvPolynomial_zero`, `toMvPolynomial_eval_eq_apply`, `toMvPolynomial_mul`, `toMvPolynomial_constantCoeff`, `toMvPolynomial_isHomogeneous`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toMvPolynomial_add` 📖	mathematical	—	`toMvPolynomial` `Matrix` `add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Pi.instAdd` `MvPolynomial` `MvPolynomial.commSemiring`	—	`Finset.sum_congr` `map_add` `SemilinearMapClass.toAddHomClass` `LinearMap.semilinearMapClass` `Finset.sum_add_distrib`
`toMvPolynomial_constantCoeff` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.constantCoeff` `toMvPolynomial` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`Finset.sum_congr` `map_sum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `MvPolynomial.constantCoeff_X` `MulZeroClass.mul_zero` `Finset.sum_const_zero`
`toMvPolynomial_eval_eq_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `RingHom.instFunLike` `MvPolynomial.eval` `toMvPolynomial` `mulVec` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`map_sum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Finset.sum_congr` `MvPolynomial.eval_monomial` `Finsupp.prod_single_index` `pow_zero` `pow_one`
`toMvPolynomial_isHomogeneous` 📖	mathematical	—	`MvPolynomial.IsHomogeneous` `toMvPolynomial`	—	`MvPolynomial.IsHomogeneous.sum` `MvPolynomial.isHomogeneous_monomial` `Finset.sum_congr` `Finsupp.support_single_ne_zero` `one_ne_zero` `Finset.sum_singleton` `Finsupp.single_eq_same`
`toMvPolynomial_map` 📖	mathematical	—	`toMvPolynomial` `map` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `MvPolynomial` `MvPolynomial.commSemiring` `MvPolynomial.map`	—	`Finset.sum_congr` `map_sum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `MvPolynomial.map_monomial`
`toMvPolynomial_mul` 📖	mathematical	—	`toMvPolynomial` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DFunLike.coe` `AlgHom` `MvPolynomial` `MvPolynomial.commSemiring` `MvPolynomial.algebra` `Algebra.id` `AlgHom.funLike` `MvPolynomial.bind₁`	—	`Finset.sum_congr` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Finset.sum_comm` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `MvPolynomial.eval₂_monomial` `Finsupp.prod_single_index` `pow_zero` `pow_one` `Finset.mul_sum` `MvPolynomial.monomial_mul` `zero_add`
`toMvPolynomial_one` 📖	mathematical	—	`toMvPolynomial` `Matrix` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `MvPolynomial.X`	—	`toMvPolynomial.eq_1` `Finset.sum_eq_single` `one_apply_ne` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `one_apply_eq` `one_mul`
`toMvPolynomial_totalDegree_le` 📖	mathematical	—	`MvPolynomial.totalDegree` `toMvPolynomial`	—	`MvPolynomial.IsHomogeneous.totalDegree_le` `toMvPolynomial_isHomogeneous`
`toMvPolynomial_zero` 📖	mathematical	—	`toMvPolynomial` `Matrix` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Pi.instZero` `MvPolynomial` `MvPolynomial.commSemiring`	—	`MvPolynomial.ext` `Finset.sum_congr` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Finset.sum_const_zero`

---

← Back to Index