MvPolynomial

📁 Source: Mathlib/LinearAlgebra/Matrix/MvPolynomial.lean

Statistics

Metric	Count
Definitions mvPolynomialX	1
Theorems det_mvPolynomialX_ne_zero, mvPolynomialX_apply, mvPolynomialX_mapMatrix_aeval, mvPolynomialX_mapMatrix_eval, mvPolynomialX_map_eval₂	5
Total	6

Matrix

Definitions

Name	Category	Theorems
mvPolynomialX 📖	CompOp	4 math math: mvPolynomialX_apply, mvPolynomialX_mapMatrix_eval, mvPolynomialX_map_eval₂, mvPolynomialX_mapMatrix_aeval

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_mvPolynomialX_ne_zero 📖	—	—	—	—	mvPolynomialX_mapMatrix_eval zero_ne_one NeZero.one map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingHom.map_det det_one
mvPolynomialX_apply 📖	mathematical	—	mvPolynomialX MvPolynomial.X	—	—
mvPolynomialX_mapMatrix_aeval 📖	mathematical	—	DFunLike.coe AlgHom Matrix MvPolynomial semiring CommSemiring.toSemiring MvPolynomial.commSemiring instAlgebra MvPolynomial.algebra Algebra.id AlgHom.funLike AlgHom.mapMatrix MvPolynomial.aeval mvPolynomialX	—	mvPolynomialX_map_eval₂
mvPolynomialX_mapMatrix_eval 📖	mathematical	—	DFunLike.coe RingHom Matrix MvPolynomial nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike RingHom.mapMatrix MvPolynomial.eval mvPolynomialX	—	mvPolynomialX_map_eval₂
mvPolynomialX_map_eval₂ 📖	mathematical	—	map MvPolynomial mvPolynomialX MvPolynomial.eval₂	—	ext MvPolynomial.eval₂_X

---

← Back to Index