Coeff

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

Statistics

Metric	Count
Definitions `constantCoeff`, `lcoeff`, `lsum`	3
Theorems `C_dvd_iff_dvd_coeff`, `C_mul'`, `card_support_binomial`, `card_support_mul_le`, `card_support_trinomial`, `charP`, `charZero`, `coeff_C_mul`, `coeff_C_mul_X`, `coeff_C_mul_X_pow`, `coeff_X_add_C_pow`, `coeff_X_add_one_pow`, `coeff_X_mul`, `coeff_X_mul_zero`, `coeff_X_pow`, `coeff_X_pow_mul`, `coeff_X_pow_mul'`, `coeff_X_pow_self`, `coeff_add`, `coeff_intCast_mul`, `coeff_list_sum`, `coeff_list_sum_map`, `coeff_monomial_mul`, `coeff_monomial_zero_mul`, `coeff_mul`, `coeff_mul_C`, `coeff_mul_X`, `coeff_mul_X_pow`, `coeff_mul_X_pow'`, `coeff_mul_X_zero`, `coeff_mul_intCast`, `coeff_mul_monomial`, `coeff_mul_monomial_zero`, `coeff_mul_natCast`, `coeff_mul_ofNat`, `coeff_natCast_mul`, `coeff_ofNat_mul`, `coeff_one_add_X_pow`, `coeff_smul`, `coeff_sum`, `constantCoeff_apply`, `constantCoeff_surjective`, `finset_sum_coeff`, `intCast_coeff_zero`, `intCast_inj`, `isRegular_X`, `isRegular_X_pow`, `isUnit_C`, `lcoeff_apply`, `lsum_apply`, `mul_X_pow_eq_zero`, `mul_coeff_one`, `mul_coeff_zero`, `natCast_coeff_zero`, `natCast_inj`, `one_add_X_pow_sub_X_pow`, `smul_eq_C_mul`, `support_binomial`, `support_smul`, `support_trinomial`, `update_eq_add_sub_coeff`	61
Total	64

Polynomial

Definitions

Name	Category	Theorems
`constantCoeff` 📖	CompOp	7 math math: `constantCoeff_apply`, `ker_constantCoeff`, `LinearMap.hasEigenvalue_zero_tfae`, `evalRingHom_zero`, `LinearMap.charpoly_constantCoeff_eq_zero_iff`, `constantCoeff_surjective`, `LinearMap.not_hasEigenvalue_zero_tfae`
`lcoeff` 📖	CompOp	3 math math: `lcoeff_comp_mapAlgHom_eq`, `lcoeff_apply`, `coeff_list_sum`
`lsum` 📖	CompOp	1 math math: `lsum_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`C_dvd_iff_dvd_coeff` 📖	mathematical	—	`Polynomial` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `Semiring.toNonUnitalSemiring` `semiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C` `coeff`	—	`coeff_C_mul` `dvd_mul_right` `ext` `Finset.sum_congr` `finset_sum_coeff` `coeff_monomial` `Finset.sum_ite_eq'` `MulZeroClass.mul_zero`
`C_mul'` 📖	mathematical	—	`Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `SMulZeroClass.toSMul` `instZero` `smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instDistribSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`ext` `coeff_C_mul` `coeff_smul` `smul_eq_mul`
`card_support_binomial` 📖	mathematical	—	`Finset.card` `support` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`support_binomial` `Finset.card_insert_of_notMem` `Finset.mem_singleton` `Finset.card_singleton`
`card_support_mul_le` 📖	mathematical	—	`Finset.card` `support` `Polynomial` `instMul`	—	`support_toFinsupp` `toFinsupp_mul` `Finset.card_le_card` `AddMonoidAlgebra.support_mul` `Finset.card_image₂_le`
`card_support_trinomial` 📖	mathematical	—	`Finset.card` `support` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`support_trinomial` `Finset.card_insert_of_notMem` `Finset.mem_insert` `LT.lt.ne` `Finset.mem_singleton` `LT.lt.trans` `Finset.card_singleton`
`charP` 📖	mathematical	—	`CharP` `Polynomial` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `semiring`	—	`CharP.cast_eq_zero_iff` `map_natCast` `RingHom.instRingHomClass` `C_0`
`charZero` 📖	mathematical	—	`CharZero` `Polynomial` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `semiring`	—	—
`coeff_C_mul` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`AddMonoidAlgebra.single_zero_mul_apply`
`coeff_C_mul_X` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `X` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`pow_one` `coeff_C_mul_X_pow`
`coeff_C_mul_X_pow` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`C_mul_X_pow_eq_monomial` `coeff_monomial`
`coeff_X_add_C_pow` 📖	mathematical	—	`coeff` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `instAdd` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.choose`	—	`Commute.add_pow` `commute_X` `lcoeff_apply` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Finset.sum_congr` `coeff_mul_C` `Finset.sum_eq_single` `coeff_X_pow` `MulZeroClass.zero_mul` `coeff_X_pow_self` `one_mul` `Nat.choose_eq_zero_of_lt` `Nat.cast_zero` `MulZeroClass.mul_zero`
`coeff_X_add_one_pow` 📖	mathematical	—	`coeff` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `instAdd` `X` `instOne` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Nat.choose`	—	`C_1` `coeff_X_add_C_pow` `one_pow` `one_mul`
`coeff_X_mul` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `X`	—	`Commute.eq` `commute_X` `coeff_mul_X`
`coeff_X_mul_zero` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `X` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`mul_coeff_zero` `coeff_X_zero` `MulZeroClass.zero_mul`
`coeff_X_pow` 📖	mathematical	—	`coeff` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_mul`
`coeff_X_pow_mul` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X`	—	`Commute.eq` `commute_X_pow` `coeff_mul_X_pow`
`coeff_X_pow_mul'` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Commute.eq` `commute_X_pow` `coeff_mul_X_pow'`
`coeff_X_pow_self` 📖	mathematical	—	`coeff` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`coeff_X_pow`
`coeff_add` 📖	mathematical	—	`coeff` `Polynomial` `instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`Finsupp.add_apply`
`coeff_intCast_mul` 📖	mathematical	—	`coeff` `Ring.toSemiring` `Polynomial` `instMul` `instIntCast` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`coeff_C_mul`
`coeff_list_sum` 📖	mathematical	—	`coeff` `Polynomial` `instAdd` `instZero` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `DFunLike.coe` `LinearMap` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `semiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `lcoeff`	—	`map_list_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`coeff_list_sum_map` 📖	mathematical	—	`coeff` `Polynomial` `instAdd` `instZero` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`coeff_list_sum`
`coeff_monomial_mul` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`C_mul_X_pow_eq_monomial` `mul_assoc` `coeff_C_mul` `X_pow_mul` `coeff_mul_X_pow`
`coeff_monomial_zero_mul` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`coeff_monomial_mul`
`coeff_mul` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `Finset.Nat.instHasAntidiagonal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`Finset.sum_congr` `AddMonoidAlgebra.mul_apply_antidiagonal` `Finset.HasAntidiagonal.mem_antidiagonal`
`coeff_mul_C` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`AddMonoidAlgebra.mul_single_zero_apply`
`coeff_mul_X` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `X`	—	`pow_one` `coeff_mul_X_pow`
`coeff_mul_X_pow` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X`	—	`coeff_mul` `Finset.sum_eq_single` `coeff_X_pow` `MulZeroClass.mul_zero` `mul_one`
`coeff_mul_X_pow'` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `coeff_mul_X_pow` `add_tsub_cancel_right` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `coeff_mul` `Finset.sum_eq_zero` `coeff_X_pow` `LT.lt.ne` `LE.le.trans_lt` `le_of_add_le_right` `Eq.le` `Finset.HasAntidiagonal.mem_antidiagonal` `not_le` `MulZeroClass.mul_zero`
`coeff_mul_X_zero` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `X` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`mul_coeff_zero` `coeff_X_zero` `MulZeroClass.mul_zero`
`coeff_mul_intCast` 📖	mathematical	—	`coeff` `Ring.toSemiring` `Polynomial` `instMul` `instIntCast` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`coeff_mul_C`
`coeff_mul_monomial` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`C_mul_X_pow_eq_monomial` `X_pow_mul` `mul_assoc` `coeff_mul_C` `coeff_mul_X_pow`
`coeff_mul_monomial_zero` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`coeff_mul_monomial`
`coeff_mul_natCast` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `instNatCast` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`coeff_mul_C`
`coeff_mul_ofNat` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`coeff_mul_C`
`coeff_natCast_mul` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `instNatCast` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`coeff_C_mul`
`coeff_ofNat_mul` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`coeff_C_mul`
`coeff_one_add_X_pow` 📖	mathematical	—	`coeff` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `instAdd` `instOne` `X` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Nat.choose`	—	`add_comm` `coeff_X_add_one_pow`
`coeff_smul` 📖	mathematical	—	`coeff` `Polynomial` `SMulZeroClass.toSMul` `instZero` `smulZeroClass` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`coeff_sum` 📖	mathematical	—	`coeff` `sum` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `semiring`	—	`finset_sum_coeff` `Finset.sum_congr`
`constantCoeff_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `constantCoeff` `coeff`	—	—
`constantCoeff_surjective` 📖	mathematical	—	`Polynomial` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `constantCoeff`	—	`coeff_C_zero`
`finset_sum_coeff` 📖	mathematical	—	`coeff` `Finset.sum` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `semiring`	—	`map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`intCast_coeff_zero` 📖	mathematical	—	`coeff` `Ring.toSemiring` `Polynomial` `instIntCast` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	`Int.cast_natCast` `coeff_natCast_ite` `Int.cast_negSucc` `Nat.cast_add` `Nat.cast_one` `neg_add_rev` `coeff_add` `coeff_neg` `coeff_one_zero`
`intCast_inj` 📖	mathematical	—	`Polynomial` `Ring.toSemiring` `instIntCast`	—	`intCast_coeff_zero`
`isRegular_X` 📖	mathematical	—	`IsRegular` `Polynomial` `instMul` `X`	—	`isRegular_X_pow` `pow_one`
`isRegular_X_pow` 📖	mathematical	—	`IsRegular` `Polynomial` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X`	—	`ext` `coeff_X_pow_mul` `IsLeftRegular.right_of_commute` `commute_X_pow`
`isUnit_C` 📖	mathematical	—	`IsUnit` `Polynomial` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	—	`coeff_C_zero` `IsUnit.map` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`lcoeff_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `lcoeff` `coeff`	—	—
`lsum_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `module` `LinearMap.instFunLike` `lsum` `sum`	—	—
`mul_X_pow_eq_zero` 📖	—	`Polynomial` `instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `instZero`	—	—	`ext` `coeff_mul_X_pow` `ext_iff`
`mul_coeff_one` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul`	—	`coeff_mul` `Finset.Nat.antidiagonal_eq_map` `Finset.sum_map` `Finset.sum_congr` `Finset.sum_range_succ` `Finset.sum_singleton` `tsub_zero` `Nat.instOrderedSub` `tsub_self` `Nat.instCanonicallyOrderedAdd`
`mul_coeff_zero` 📖	mathematical	—	`coeff` `Polynomial` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`coeff_mul` `Finset.sum_congr` `Finset.antidiagonal_zero` `Nat.instCanonicallyOrderedAdd` `Finset.sum_singleton`
`natCast_coeff_zero` 📖	mathematical	—	`coeff` `Polynomial` `instNatCast` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`coeff_natCast_ite`
`natCast_inj` 📖	mathematical	—	`Polynomial` `instNatCast`	—	`coeff_natCast_ite`
`one_add_X_pow_sub_X_pow` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instSub` `CommRing.toRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `instAdd` `instOne` `X` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Finset.range` `instNSMul` `Nat.choose`	—	`ext` `coeff_sub` `coeff_one_add_X_pow` `coeff_X_pow` `Finset.sum_congr` `nsmul_eq_mul` `finset_sum_coeff` `coeff_natCast_mul` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `Finset.sum_ite_eq` `Nat.choose_self` `Nat.cast_one` `sub_self` `sub_zero` `Nat.choose_eq_zero_of_lt` `Nat.cast_zero`
`smul_eq_C_mul` 📖	mathematical	—	`Polynomial` `SMulZeroClass.toSMul` `instZero` `smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instDistribSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instMul` `DFunLike.coe` `RingHom` `semiring` `RingHom.instFunLike` `C`	—	`coeff_smul` `coeff_C_mul`
`support_binomial` 📖	mathematical	—	`support` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `Finset` `Finset.instInsert` `Finset.instSingleton`	—	`subset_antisymm` `Finset.instAntisymmSubset` `support_binomial'` `coeff_add` `coeff_C_mul` `coeff_X_pow_self` `mul_one` `coeff_X_pow` `MulZeroClass.mul_zero` `zero_add` `add_zero`
`support_smul` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `support` `Polynomial` `SMulZeroClass.toSMul` `instZero` `smulZeroClass`	—	`mem_support_iff` `Mathlib.Tactic.Contrapose.contrapose₄` `coeff_smul` `smul_zero`
`support_trinomial` 📖	mathematical	—	`support` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `Finset` `Finset.instInsert` `Finset.instSingleton`	—	`subset_antisymm` `Finset.instAntisymmSubset` `support_trinomial'` `coeff_add` `coeff_C_mul` `coeff_X_pow_self` `mul_one` `coeff_X_pow` `LT.lt.ne` `LT.lt.ne'` `LT.lt.trans` `MulZeroClass.mul_zero` `add_zero` `zero_add`
`update_eq_add_sub_coeff` 📖	mathematical	—	`update` `Ring.toSemiring` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `coeff` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`ext` `coeff_update_apply` `coeff_add` `coeff_C_mul_X_pow` `add_sub_cancel` `add_zero`

---

← Back to Index