Polynomial

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

Statistics

Metric	Count
Definitions	0
Theorems coeff_det_X_add_C_card, coeff_det_X_add_C_zero, leadingCoeff_det_X_one_add_C, natDegree_det_X_add_C_le	4
Total	4

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_det_X_add_C_card 📖	mathematical	—	coeff CommSemiring.toSemiring CommRing.toCommSemiring Matrix.det Polynomial commRing Matrix Matrix.add instAdd Matrix.smul Algebra.toSMul commSemiring Algebra.id X Matrix.map DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Fintype.card	—	Matrix.det_apply finset_sum_coeff Finset.sum_congr mul_one Finset.prod_congr X_mul_C coeff_add coeff_C_mul coeff_X_one coeff_C add_zero coeff_prod_of_natDegree_le le_trans natDegree_add_le_of_le natDegree_mul_le_of_le natDegree_X_le Mathlib.Tactic.ComputeDegree.natDegree_C_le Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat sup_of_le_left Mathlib.Meta.NormNum.isNat_le_true IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.cast_zero Nat.cast_one le_refl coeff_smul
coeff_det_X_add_C_zero 📖	mathematical	—	coeff CommSemiring.toSemiring CommRing.toCommSemiring Matrix.det Polynomial commRing Matrix Matrix.add instAdd Matrix.smul Algebra.toSMul commSemiring Algebra.id X Matrix.map DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	Matrix.det_apply finset_sum_coeff Finset.sum_congr coeff_zero_prod Finset.prod_congr X_mul_C coeff_add mul_coeff_zero coeff_C_zero coeff_X_zero MulZeroClass.mul_zero zero_add coeff_smul
leadingCoeff_det_X_one_add_C 📖	mathematical	—	leadingCoeff CommSemiring.toSemiring CommRing.toCommSemiring Matrix.det Polynomial commRing Matrix Matrix.add instAdd Matrix.smul Algebra.toSMul commSemiring Algebra.id X Matrix.one instZero instOne Matrix.map DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	subsingleton_or_nontrivial Matrix.det_one coeff_det_X_add_C_card leadingCoeff.eq_1 Matrix.det.congr_simp Matrix.map_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass LE.le.eq_or_lt natDegree_det_X_add_C_le coeff_eq_zero_of_natDegree_lt NeZero.one
natDegree_det_X_add_C_le 📖	mathematical	—	natDegree CommSemiring.toSemiring CommRing.toCommSemiring Matrix.det Polynomial commRing Matrix Matrix.add instAdd Matrix.smul Algebra.toSMul commSemiring Algebra.id X Matrix.map DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Fintype.card	—	Matrix.det_apply LE.le.trans natDegree_sum_le Multiset.max_le_of_forall_le Multiset.map_congr Int.units_eq_one_or one_smul le_refl Units.neg_smul natDegree_neg natDegree_prod_le Finset.sum_le_card_nsmul IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid le_trans natDegree_add_le_of_le natDegree_mul_le_of_le natDegree_X_le Mathlib.Tactic.ComputeDegree.natDegree_C_le Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat sup_of_le_left Mathlib.Meta.NormNum.isNat_le_true IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.cast_zero Nat.cast_one mul_one

---

← Back to Index