Univ

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

Statistics

Metric	Count
Definitions univ	1
Theorems optionEquivLeft_symm_univ_isHomogeneous, univ_coeff_card, univ_coeff_eval₂Hom, univ_coeff_isHomogeneous, univ_map_eval₂Hom, univ_map_map, univ_monic, univ_natDegree	8
Total	9

Matrix.charpoly

Definitions

Name	Category	Theorems
univ 📖	CompOp	9 math math: univ_map_map, univ_monic, univ_coeff_eval₂Hom, optionEquivLeft_symm_univ_isHomogeneous, univ_coeff_isHomogeneous, LinearMap.polyCharpoly_eq_of_basis, univ_natDegree, univ_map_eval₂Hom, univ_coeff_card

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
optionEquivLeft_symm_univ_isHomogeneous 📖	mathematical	—	MvPolynomial.IsHomogeneous CommRing.toCommSemiring DFunLike.coe AlgEquiv Polynomial MvPolynomial CommSemiring.toSemiring MvPolynomial.commSemiring Polynomial.semiring Polynomial.algebraOfAlgebra MvPolynomial.algebra Algebra.id AlgEquiv.instFunLike AlgEquiv.symm MvPolynomial.optionEquivLeft univ Fintype.card	—	Finset.sum_const mul_one zero_add Matrix.det.congr_simp Matrix.det_apply' Finset.sum_congr Finset.prod_congr map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass map_intCast AlgHomClass.toRingHomClass map_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_sub Polynomial.aevalTower_C MvPolynomial.rename_X MvPolynomial.IsHomogeneous.sum MvPolynomial.IsHomogeneous.mul MvPolynomial.isHomogeneous_C MvPolynomial.IsHomogeneous.prod Polynomial.aevalTower_X map_zero MonoidWithZeroHomClass.toZeroHomClass AlgHom.algHomClass zero_sub MvPolynomial.IsHomogeneous.neg MvPolynomial.isHomogeneous_X
univ_coeff_card 📖	mathematical	—	Polynomial.coeff MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring univ Fintype.card AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing MvPolynomial.instCommRingMvPolynomial	—	univ_natDegree Int.instNontrivial Polynomial.Monic.leadingCoeff univ_monic univ_map_map Polynomial.coeff_map map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
univ_coeff_eval₂Hom 📖	mathematical	—	DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.eval₂Hom Polynomial.coeff univ Matrix.charpoly Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike Matrix.of	—	univ_map_eval₂Hom Polynomial.coeff_map
univ_coeff_isHomogeneous 📖	mathematical	Fintype.card	MvPolynomial.IsHomogeneous CommRing.toCommSemiring Polynomial.coeff MvPolynomial CommSemiring.toSemiring MvPolynomial.commSemiring univ	—	MvPolynomial.IsHomogeneous.coeff_isHomogeneous_of_optionEquivLeft_symm Finite.instProd Finite.of_fintype optionEquivLeft_symm_univ_isHomogeneous
univ_map_eval₂Hom 📖	mathematical	—	Polynomial.map MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.eval₂Hom univ Matrix.charpoly DFunLike.coe Equiv Matrix EquivLike.toFunLike Equiv.instEquivLike Matrix.of	—	univ.eq_1 Matrix.charpoly_map MvPolynomial.coe_eval₂Hom Matrix.mvPolynomialX_map_eval₂ congr_simp
univ_map_map 📖	mathematical	—	Polynomial.map MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.map univ	—	MvPolynomial.map.eq_1 univ_map_eval₂Hom
univ_monic 📖	mathematical	—	Polynomial.Monic MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring univ	—	Matrix.charpoly_monic
univ_natDegree 📖	mathematical	—	Polynomial.natDegree MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring univ Fintype.card	—	Matrix.charpoly_natDegree_eq_dim MvPolynomial.nontrivial_of_nontrivial

---

← Back to Index