EraseLead

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

Statistics

Metric	Count
Definitions `eraseLead`	1
Theorems `card_support_eq`, `card_support_eq'`, `card_support_eq_one`, `card_support_eq_one_of_eraseLead_eq_zero`, `card_support_eq_three`, `card_support_eq_two`, `card_support_eraseLead`, `card_support_eraseLead'`, `card_support_eraseLead_add_one`, `card_support_le_one_of_eraseLead_eq_zero`, `degree_eraseLead_lt`, `eraseLead_C`, `eraseLead_C_mul_X`, `eraseLead_C_mul_X_pow`, `eraseLead_X`, `eraseLead_X_pow`, `eraseLead_add_C_mul_X_pow`, `eraseLead_add_monomial_natDegree_leadingCoeff`, `eraseLead_add_of_degree_lt_left`, `eraseLead_add_of_degree_lt_right`, `eraseLead_add_of_natDegree_lt_left`, `eraseLead_add_of_natDegree_lt_right`, `eraseLead_coeff`, `eraseLead_coeff_natDegree`, `eraseLead_coeff_of_ne`, `eraseLead_degree_le`, `eraseLead_monomial`, `eraseLead_mul_eq_mul_eraseLead_of_nextCoeff_zero`, `eraseLead_natDegree_le`, `eraseLead_natDegree_le_aux`, `eraseLead_natDegree_lt`, `eraseLead_natDegree_lt_or_eraseLead_eq_zero`, `eraseLead_ne_zero`, `eraseLead_support`, `eraseLead_support_card_lt`, `eraseLead_zero`, `induction_with_natDegree_le`, `leadingCoeff_eraseLead_eq_nextCoeff`, `lt_natDegree_of_mem_eraseLead_support`, `map_natDegree_eq_natDegree`, `map_natDegree_eq_sub`, `mono_map_natDegree_eq`, `natDegree_eraseLead`, `natDegree_eraseLead_add_one`, `natDegree_eraseLead_le_of_nextCoeff_eq_zero`, `natDegree_notMem_eraseLead_support`, `natDegree_pos_of_eraseLead_ne_zero`, `ne_natDegree_of_mem_eraseLead_support`, `nextCoeff_eq_zero_of_eraseLead_eq_zero`, `self_sub_C_mul_X_pow`, `self_sub_monomial_natDegree_leadingCoeff`, `two_le_natDegree_of_nextCoeff_eraseLead`	52
Total	53

Polynomial

Definitions

Name	Category	Theorems
`eraseLead` 📖	CompOp	45 math math: `eraseLead_monomial`, `eraseLead_natDegree_lt_or_eraseLead_eq_zero`, `eraseLead_X_pow`, `eraseLead_support`, `eraseLead_add_C_mul_X_pow`, `card_support_eraseLead_add_one`, `signVariations_le_eraseLead_succ`, `natDegree_notMem_eraseLead_support`, `natDegree_eraseLead_add_one`, `self_sub_monomial_natDegree_leadingCoeff`, `card_support_eraseLead'`, `leadingCoeff_cons_eraseLead`, `eraseLead_natDegree_le`, `eraseLead_coeff`, `coeffList_eraseLead`, `degree_eraseLead_lt`, `signVariations_eraseLead`, `eraseLead_C_mul_X`, `signVariations_eraseLead_le`, `content_mul_aux`, `eraseLead_add_of_degree_lt_right`, `eraseLead_add_of_degree_lt_left`, `eraseLead_add_monomial_natDegree_leadingCoeff`, `eraseLead_zero`, `eraseLead_degree_le`, `eraseLead_C_mul_X_pow`, `eraseLead_X`, `signVariations_eraseLead_mul_X_sub_C`, `card_support_eraseLead`, `eraseLead_C`, `natDegree_eraseLead`, `eraseLead_support_card_lt`, `leadingCoeff_eraseLead_eq_nextCoeff`, `eraseLead_mul_eq_mul_eraseLead_of_nextCoeff_zero`, `eraseLead_coeff_natDegree`, `signVariations_X_sub_C_mul_eraseLead_le`, `eraseLead_natDegree_lt`, `signVariations_eq_eraseLead_add_ite`, `content_eq_gcd_leadingCoeff_content_eraseLead`, `eraseLead_coeff_of_ne`, `eraseLead_natDegree_le_aux`, `eraseLead_add_of_natDegree_lt_left`, `natDegree_eraseLead_le_of_nextCoeff_eq_zero`, `eraseLead_add_of_natDegree_lt_right`, `self_sub_C_mul_X_pow`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_support_eq` 📖	mathematical	—	`Finset.card` `support` `Finset.sum` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `semiring` `Finset.univ` `Fin.fintype` `instMul` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`card_support_eq_zero` `card_support_eraseLead'` `LT.lt.ne` `Fin.range_castSucc` `lt_of_lt_of_le` `Function.Injective.extend_apply` `StrictMono.injective` `Fin.strictMono_castSucc` `StrictMono.lt_iff_lt` `Function.extend_apply'` `lt_natDegree_of_mem_eraseLead_support` `mem_support_iff` `finset_sum_coeff` `Finset.sum_eq_single` `coeff_C_mul` `coeff_X_pow` `MulZeroClass.mul_zero` `Finset.mem_univ` `coeff_X_pow_self` `mul_one` `leadingCoeff_eq_zero` `Fin.sum_univ_castSucc` `Finset.sum_congr` `eraseLead_add_C_mul_X_pow` `card_support_eq'`
`card_support_eq'` 📖	mathematical	—	`Finset.card` `support` `Finset.sum` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `semiring` `Finset.univ` `Fin.fintype` `instMul` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`finset_sum_coeff` `Finset.sum_congr` `coeff_C_mul_X_pow` `Finset.exists_ne_zero_of_sum_ne_zero` `ite_ne_right_iff` `Finset.sum_eq_single_of_mem` `Finset.mem_univ` `Finset.card_image_of_injective` `Finset.card_fin`
`card_support_eq_one` 📖	mathematical	—	`Finset.card` `support` `Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`card_support_eq` `Fin.sum_univ_one` `support_C_mul_X_pow` `Finset.card_singleton`
`card_support_eq_one_of_eraseLead_eq_zero` 📖	mathematical	`eraseLead` `Polynomial` `instZero`	`Finset.card` `support`	—	`card_support_eraseLead_add_one` `card_support_eq_zero`
`card_support_eq_three` 📖	mathematical	—	`Finset.card` `support` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`card_support_eq` `Fin.sum_univ_castSucc` `Fin.sum_univ_one` `card_support_trinomial`
`card_support_eq_two` 📖	mathematical	—	`Finset.card` `support` `Polynomial` `instAdd` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`card_support_eq` `Fin.sum_univ_castSucc` `Fin.sum_univ_one` `card_support_binomial` `LT.lt.ne`
`card_support_eraseLead` 📖	mathematical	—	`Finset.card` `support` `eraseLead`	—	`eraseLead_zero` `support_zero` `Finset.card_empty` `card_support_eraseLead_add_one` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`card_support_eraseLead'` 📖	mathematical	`Finset.card` `support`	`eraseLead`	—	`card_support_eraseLead` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`card_support_eraseLead_add_one` 📖	mathematical	—	`Finset.card` `support` `eraseLead`	—	`card_support_eq_zero` `eraseLead_support` `Finset.card_erase_of_mem` `natDegree_mem_support_of_nonzero`
`card_support_le_one_of_eraseLead_eq_zero` 📖	mathematical	`eraseLead` `Polynomial` `instZero`	`Finset.card` `support`	—	`Nat.instCanonicallyOrderedAdd` `le_of_eq` `card_support_eq_one_of_eraseLead_eq_zero`
`degree_eraseLead_lt` 📖	mathematical	—	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `eraseLead`	—	`degree_erase_lt`
`eraseLead_C` 📖	mathematical	—	`eraseLead` `DFunLike.coe` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `instZero`	—	`eraseLead_monomial`
`eraseLead_C_mul_X` 📖	mathematical	—	`eraseLead` `Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `X` `instZero`	—	`pow_one` `eraseLead_C_mul_X_pow`
`eraseLead_C_mul_X_pow` 📖	mathematical	—	`eraseLead` `Polynomial` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `instZero`	—	`C_mul_X_pow_eq_monomial` `eraseLead_monomial`
`eraseLead_X` 📖	mathematical	—	`eraseLead` `X` `Polynomial` `instZero`	—	`eraseLead_monomial`
`eraseLead_X_pow` 📖	mathematical	—	`eraseLead` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `instZero`	—	`X_pow_eq_monomial` `eraseLead_monomial`
`eraseLead_add_C_mul_X_pow` 📖	mathematical	—	`Polynomial` `instAdd` `eraseLead` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `leadingCoeff` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `natDegree`	—	`C_mul_X_pow_eq_monomial` `eraseLead_add_monomial_natDegree_leadingCoeff`
`eraseLead_add_monomial_natDegree_leadingCoeff` 📖	mathematical	—	`Polynomial` `instAdd` `eraseLead` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `natDegree` `leadingCoeff`	—	`add_comm` `monomial_add_erase`
`eraseLead_add_of_degree_lt_left` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree`	`eraseLead` `Polynomial` `instAdd`	—	`ext` `eraseLead_coeff` `natDegree_add_eq_left_of_degree_lt` `coeff_add` `eraseLead_coeff_natDegree` `zero_add` `coeff_eq_zero_of_degree_lt` `lt_of_lt_of_le` `degree_le_natDegree`
`eraseLead_add_of_degree_lt_right` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree`	`eraseLead` `Polynomial` `instAdd`	—	`ext` `eraseLead_coeff` `natDegree_add_eq_right_of_degree_lt` `coeff_add` `eraseLead_coeff_natDegree` `add_zero` `coeff_eq_zero_of_degree_lt` `lt_of_lt_of_le` `degree_le_natDegree`
`eraseLead_add_of_natDegree_lt_left` 📖	mathematical	`natDegree`	`eraseLead` `Polynomial` `instAdd`	—	`eraseLead_add_of_degree_lt_left` `degree_lt_degree`
`eraseLead_add_of_natDegree_lt_right` 📖	mathematical	`natDegree`	`eraseLead` `Polynomial` `instAdd`	—	`eraseLead_add_of_degree_lt_right` `degree_lt_degree`
`eraseLead_coeff` 📖	mathematical	—	`coeff` `eraseLead` `natDegree` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`coeff_erase`
`eraseLead_coeff_natDegree` 📖	mathematical	—	`coeff` `eraseLead` `natDegree` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`eraseLead_coeff`
`eraseLead_coeff_of_ne` 📖	mathematical	—	`coeff` `eraseLead`	—	`eraseLead_coeff`
`eraseLead_degree_le` 📖	mathematical	—	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `degree` `eraseLead`	—	`degree_erase_le`
`eraseLead_monomial` 📖	mathematical	—	`eraseLead` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `instZero`	—	`monomial_zero_right` `eraseLead_zero` `eraseLead.eq_1` `natDegree_monomial` `erase_monomial`
`eraseLead_mul_eq_mul_eraseLead_of_nextCoeff_zero` 📖	mathematical	`nextCoeff` `Ring.toSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`eraseLead` `Polynomial` `instMul` `instSub` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`MulZeroClass.mul_zero` `eraseLead_zero` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `pow_one` `one_mul` `map_neg` `RingHomClass.toAddMonoidHomClass` `pow_zero` `mul_one` `card_support_binomial` `one_ne_zero` `NeZero.one` `neg_ne_zero` `card_support_mul_le` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing` `Nat.cast_mul` `Mathlib.Tactic.Linarith.mul_nonpos` `Nat.cast_one` `card_support_le_one_of_eraseLead_eq_zero` `Mathlib.Meta.NormNum.isNat_lt_true` `Int.instCharZero` `card_support_eq_zero` `Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt` `Mathlib.Tactic.Linarith.natCast_nonneg` `Nat.cast_zero` `eraseLead_support_card_lt` `mul_ne_zero` `instNoZeroDivisors` `X_sub_C_ne_zero` `natDegree_mul` `natDegree_X_sub_C` `add_comm` `two_le_natDegree_of_nextCoeff_eraseLead` `nextCoeff.eq_1` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `coeff_X_sub_C_mul` `zero_sub` `ext` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `neg_eq_zero` `sub_eq_zero_of_eq` `Nat.cast_add` `natDegree_eraseLead_add_one` `self_sub_monomial_natDegree_leadingCoeff` `coeff_sub` `coeff_monomial` `LT.lt.ne'` `mul_sub` `sub_zero` `eq_sub_iff_add_eq` `add_eq_left` `mul_coeff_zero` `coeff_X_zero` `coeff_C_zero` `mul_ite` `neg_mul` `coeff_eq_zero_of_natDegree_lt` `lt_imp_lt_of_le_of_le` `eraseLead_natDegree_le` `le_refl` `add_le_add_right` `natDegree_eraseLead_le_of_nextCoeff_eq_zero` `natDegree_sub_C` `natDegree_X`
`eraseLead_natDegree_le` 📖	mathematical	—	`natDegree` `eraseLead`	—	`eraseLead_natDegree_lt_or_eraseLead_eq_zero` `Nat.instCanonicallyOrderedAdd`
`eraseLead_natDegree_le_aux` 📖	mathematical	—	`natDegree` `eraseLead`	—	`natDegree_le_natDegree` `eraseLead_degree_le`
`eraseLead_natDegree_lt` 📖	mathematical	`Finset.card` `support`	`natDegree` `eraseLead`	—	`lt_of_le_of_ne` `eraseLead_natDegree_le_aux` `ne_natDegree_of_mem_eraseLead_support` `natDegree_mem_support_of_nonzero` `eraseLead_ne_zero`
`eraseLead_natDegree_lt_or_eraseLead_eq_zero` 📖	mathematical	—	`natDegree` `eraseLead` `Polynomial` `instZero`	—	`C_mul_X_pow_eq_self` `eraseLead_C_mul_X_pow` `eraseLead_natDegree_lt`
`eraseLead_ne_zero` 📖	—	`Finset.card` `support`	—	—	`card_support_eq_zero` `eraseLead_support` `LT.lt.ne` `LT.lt.trans_le` `zero_lt_one` `Nat.instZeroLEOneClass` `LE.le.trans` `tsub_le_tsub_right` `Nat.instOrderedSub` `Finset.pred_card_le_card_erase`
`eraseLead_support` 📖	mathematical	—	`support` `eraseLead` `Finset.erase` `natDegree`	—	`support_erase`
`eraseLead_support_card_lt` 📖	mathematical	—	`Finset.card` `support` `eraseLead`	—	`eraseLead_support` `Finset.card_lt_card` `Finset.erase_ssubset` `natDegree_mem_support_of_nonzero`
`eraseLead_zero` 📖	mathematical	—	`eraseLead` `Polynomial` `instZero`	—	`erase_zero`
`induction_with_natDegree_le` 📖	—	`Polynomial` `instZero` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `instAdd` `natDegree`	—	—	`eraseLead_add_C_mul_X_pow` `card_support_eq_zero` `card_support_eraseLead'` `zero_add` `leadingCoeff_ne_zero` `zero_ne_one` `LT.lt.trans_le` `eraseLead_natDegree_lt` `LE.le.trans` `Eq.ge` `le_of_eq` `natDegree_C_mul_X_pow` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `natDegree_C_mul_X_pow_le` `eraseLead_natDegree_le_aux` `leadingCoeff_eq_zero`
`leadingCoeff_eraseLead_eq_nextCoeff` 📖	mathematical	—	`leadingCoeff` `eraseLead` `nextCoeff`	—	`natDegree_pos_of_nextCoeff_ne_zero` `leadingCoeff.eq_1` `nextCoeff.eq_1` `natDegree_eraseLead` `ne_of_gt` `eraseLead_coeff_of_ne` `LT.lt.ne` `tsub_lt_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Mathlib.Meta.Positivity.pos_of_isNat` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat`
`lt_natDegree_of_mem_eraseLead_support` 📖	mathematical	`Finset` `Finset.instMembership` `support` `eraseLead`	`natDegree`	—	`LE.le.lt_of_ne` `le_natDegree_of_mem_supp` `Finset.mem_erase` `eraseLead_support`
`map_natDegree_eq_natDegree` 📖	—	`natDegree` `DFunLike.coe` `Polynomial` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial`	—	—	`map_natDegree_eq_sub` `tsub_zero` `Nat.instOrderedSub`
`map_natDegree_eq_sub` 📖	—	`DFunLike.coe` `Polynomial` `instZero` `natDegree` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial`	—	—	`mono_map_natDegree_eq` `tsub_lt_tsub_iff_right` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`mono_map_natDegree_eq` 📖	—	`DFunLike.coe` `Polynomial` `instZero` `natDegree` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial`	—	—	`induction_with_natDegree_le` `map_zero` `AddMonoidHomClass.toZeroHomClass` `Nat.instCanonicallyOrderedAdd` `natDegree_C_mul_X_pow` `C_mul_X_pow_eq_monomial` `natDegree_add_eq_right_of_natDegree_lt` `map_add` `AddMonoidHomClass.toAddHomClass` `zero_add` `Eq.le`
`natDegree_eraseLead` 📖	mathematical	—	`natDegree` `eraseLead`	—	`natDegree_pos_of_nextCoeff_ne_zero` `LE.le.antisymm` `eraseLead_natDegree_le` `le_natDegree_of_ne_zero` `eraseLead_coeff_of_ne` `LT.lt.ne` `tsub_lt_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Mathlib.Meta.Positivity.pos_of_isNat` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `nextCoeff_of_natDegree_pos`
`natDegree_eraseLead_add_one` 📖	mathematical	—	`natDegree` `eraseLead`	—	`natDegree_eraseLead` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `natDegree_pos_of_nextCoeff_ne_zero`
`natDegree_eraseLead_le_of_nextCoeff_eq_zero` 📖	mathematical	`nextCoeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`natDegree` `eraseLead`	—	`natDegree_le_pred` `eraseLead_natDegree_le` `natDegree_eq_zero` `nextCoeff_eq_zero` `eraseLead_C` `natDegree_C` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `eraseLead_coeff_of_ne` `LT.lt.ne` `tsub_lt_self` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `zero_lt_one` `Nat.instZeroLEOneClass` `nextCoeff_of_natDegree_pos`
`natDegree_notMem_eraseLead_support` 📖	mathematical	—	`Finset` `Finset.instMembership` `support` `eraseLead` `natDegree`	—	`ne_natDegree_of_mem_eraseLead_support`
`natDegree_pos_of_eraseLead_ne_zero` 📖	mathematical	—	`natDegree`	—	`eraseLead_C` `eq_C_of_natDegree_eq_zero`
`ne_natDegree_of_mem_eraseLead_support` 📖	—	`Finset` `Finset.instMembership` `support` `eraseLead`	—	—	`LT.lt.ne` `lt_natDegree_of_mem_eraseLead_support`
`nextCoeff_eq_zero_of_eraseLead_eq_zero` 📖	mathematical	`eraseLead` `Polynomial` `instZero`	`nextCoeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`leadingCoeff_ne_zero` `leadingCoeff_eraseLead_eq_nextCoeff`
`self_sub_C_mul_X_pow` 📖	mathematical	—	`Polynomial` `Ring.toSemiring` `instSub` `instMul` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `leadingCoeff` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `natDegree` `eraseLead`	—	`C_mul_X_pow_eq_monomial` `self_sub_monomial_natDegree_leadingCoeff`
`self_sub_monomial_natDegree_leadingCoeff` 📖	mathematical	—	`Polynomial` `Ring.toSemiring` `instSub` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial` `natDegree` `leadingCoeff` `eraseLead`	—	`eq_sub_iff_add_eq` `eraseLead_add_monomial_natDegree_leadingCoeff`
`two_le_natDegree_of_nextCoeff_eraseLead` 📖	mathematical	`nextCoeff` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`natDegree`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `natDegree_eq_one` `natDegree_eq_zero` `eraseLead_C` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `add_zero` `eraseLead_C_mul_X` `nextCoeff_C_mul_X_add_C`

---

← Back to Index