Coeff

📁 Source: Mathlib/Algebra/Polynomial/Eval/Coeff.lean

Statistics

Metric	Count
Definitions `piEquiv`	1
Theorems `map`, `of_map`, `coeff_map`, `coeff_map_eq_comp`, `coeff_zero_eq_eval_zero`, `coeff_zero_eq_zero_of_zero_isRoot`, `evalRingHom_zero`, `eval_intCast_map`, `eval_natCast_map`, `eval_one_map`, `eval_zero_map`, `eval₂_C_X`, `eval₂_at_zero`, `eval₂_hom`, `eval₂_map`, `hom_eval₂`, `isRoot_map_iff`, `mapRingHom_comp`, `mapRingHom_id`, `map_eq_zero_iff`, `map_id`, `map_injective`, `map_injective_iff`, `map_map`, `map_ne_zero_iff`, `map_surjective`, `map_surjective_iff`, `support_map_of_injective`, `support_map_subset`, `zero_isRoot_iff_coeff_zero_eq_zero`, `zero_isRoot_of_coeff_zero_eq_zero`	31
Total	32

Polynomial

Definitions

Name	Category	Theorems
`piEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_map` 📖	mathematical	—	`coeff` `map` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`map.eq_1` `eval₂_def` `coeff_sum` `sum.eq_1` `Finset.sum_congr` `coeff_C_mul` `coeff_X_pow` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `Finset.sum_ite_eq` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`coeff_map_eq_comp` 📖	mathematical	—	`coeff` `map` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`coeff_map`
`coeff_zero_eq_eval_zero` 📖	mathematical	—	`coeff` `eval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`pow_zero` `mul_one` `eval_eq_sum` `Finset.sum_eq_single` `zero_pow` `MulZeroClass.mul_zero`
`coeff_zero_eq_zero_of_zero_isRoot` 📖	mathematical	`IsRoot` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`coeff`	—	`zero_isRoot_iff_coeff_zero_eq_zero`
`evalRingHom_zero` 📖	mathematical	—	`evalRingHom` `Nat.instCommSemiring` `constantCoeff` `CommSemiring.toSemiring`	—	`DFunLike.ext` `coeff_zero_eq_eval_zero`
`eval_intCast_map` 📖	mathematical	—	`eval` `Ring.toSemiring` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `map` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`induction_on'` `map_add` `eval_add` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_monomial` `eval_monomial` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `map_intCast`
`eval_natCast_map` 📖	mathematical	—	`eval` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `map` `DFunLike.coe` `RingHom` `RingHom.instFunLike`	—	`induction_on'` `map_add` `eval_add` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_monomial` `eval_monomial` `RingHom.map_mul` `RingHom.map_pow` `map_natCast`
`eval_one_map` 📖	mathematical	—	`eval` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `map` `DFunLike.coe` `RingHom` `RingHom.instFunLike`	—	`induction_on'` `map_add` `eval_add` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_monomial` `eval_monomial` `one_pow` `mul_one`
`eval_zero_map` 📖	mathematical	—	`eval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `map` `DFunLike.coe` `RingHom` `RingHom.instFunLike`	—	`coeff_map`
`eval₂_C_X` 📖	mathematical	—	`eval₂` `Polynomial` `semiring` `C` `X`	—	`induction_on'` `eval₂_add` `eval₂_monomial` `smul_X_eq_monomial` `C_mul'`
`eval₂_at_zero` 📖	mathematical	—	`eval₂` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `coeff`	—	`eval₂_eq_sum` `Finset.sum_congr` `zero_pow_eq` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `Finset.sum_ite_eq'` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`eval₂_hom` 📖	mathematical	—	`eval₂` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `eval`	—	`hom_eval₂` `RingHom.comp_id`
`eval₂_map` 📖	mathematical	—	`eval₂` `map` `RingHom.comp` `Semiring.toNonAssocSemiring`	—	`eval₂_eq_eval_map` `map_map`
`hom_eval₂` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `eval₂` `RingHom.comp`	—	`eval₂_map` `eval₂_at_apply` `eval_map`
`isRoot_map_iff` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike`	`IsRoot` `map`	—	`IsRoot.of_map` `IsRoot.map`
`mapRingHom_comp` 📖	mathematical	—	`RingHom.comp` `Polynomial` `Semiring.toNonAssocSemiring` `semiring` `mapRingHom`	—	`RingHom.ext` `map_map`
`mapRingHom_id` 📖	mathematical	—	`mapRingHom` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `semiring`	—	`RingHom.ext` `map_id`
`map_eq_zero_iff` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	`map` `Polynomial` `instZero`	—	`map_eq_zero_iff` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_injective`
`map_id` 📖	mathematical	—	`map` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`coeff_map`
`map_injective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	`Polynomial` `map`	—	`ext` `coeff_map`
`map_injective_iff` 📖	mathematical	—	`Polynomial` `map` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`map_C` `map_injective`
`map_map` 📖	mathematical	—	`map` `RingHom.comp` `Semiring.toNonAssocSemiring`	—	`ext` `coeff_map`
`map_ne_zero_iff` 📖	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	—	`Iff.not` `map_eq_zero_iff`
`map_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	`Polynomial` `map`	—	`induction_on'` `map_add` `map_monomial`
`map_surjective_iff` 📖	mathematical	—	`Polynomial` `map` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`coeff_map` `coeff_C_zero` `map_surjective`
`support_map_of_injective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	`support` `map`	—	`coeff_map` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`support_map_subset` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `support` `map`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `coeff_map` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`zero_isRoot_iff_coeff_zero_eq_zero` 📖	mathematical	—	`IsRoot` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `coeff`	—	`coeff_zero_eq_eval_zero` `IsRoot.eq_1`
`zero_isRoot_of_coeff_zero_eq_zero` 📖	mathematical	`coeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`IsRoot`	—	`zero_isRoot_iff_coeff_zero_eq_zero`

Polynomial.IsRoot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map` 📖	mathematical	`Polynomial.IsRoot` `CommSemiring.toSemiring`	`Polynomial.map` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`eq_1` `Polynomial.eval_map` `Polynomial.eval₂_hom` `eq_zero` `RingHom.map_zero`
`of_map` 📖	—	`Polynomial.IsRoot` `CommSemiring.toSemiring` `Polynomial.map` `Ring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	—	`eq_1` `injective_iff_map_eq_zero'` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Polynomial.eval₂_hom` `Polynomial.eval_map`

---

← Back to Index