Basic

📁 Source: Mathlib/RingTheory/Polynomial/Basic.lean

Statistics

Metric	Count
Definitions `degreeLE`, `leadingCoeff`, `leadingCoeffNth`, `ofPolynomial`, `degreeLE`, `degreeLT`, `degreeLTEquiv`, `monicEquivDegreeLT`, `restriction`	9
Theorems `eq_zero_of_constant_mem_of_maximal`, `isPrime_map_C_iff_isPrime`, `isPrime_map_C_of_isPrime`, `is_fg_degreeLE`, `leadingCoeffNth_mono`, `mem_leadingCoeff`, `mem_leadingCoeffNth`, `mem_leadingCoeffNth_zero`, `mem_map_C_iff`, `mem_ofPolynomial`, `polynomial_mem_ideal_of_coeff_mem_ideal`, `polynomial_not_isField`, `aeval_natDegree_le`, `instFiniteOfIsEmpty`, `isNoetherianRing`, `isNoetherianRing_fin`, `isNoetherianRing_fin_0`, `ker_map`, `ker_mapAlgHom`, `map_mvPolynomial_eq_eval₂`, `mem_ideal_of_coeff_mem_ideal`, `mem_map_C_iff`, `prime_C_iff`, `prime_rename_iff`, `geom_sum`, `geom_sum'`, `coeff_prod_mem_ideal_pow_tsub`, `coeff_restriction`, `coeff_restriction'`, `degreeLE_eq_span_X_pow`, `degreeLE_mono`, `degreeLTEquiv_eq_zero_iff_eq_zero`, `degreeLT_eq_span_X_pow`, `degreeLT_mono`, `degreeLT_succ_eq_degreeLE`, `degree_restriction`, `disjoint_ker_aeval_of_isCoprime`, `eval_eq_sum_degreeLTEquiv`, `eval₂_restriction`, `exists_degree_le_of_mem_span`, `exists_degree_le_of_mem_span_of_finite`, `geom_sum_X_comp_X_add_one_eq_sum`, `instCharP`, `instExpChar`, `isNoetherianRing`, `ker_mapRingHom`, `linearIndependent_powers_iff_aeval`, `map_restriction`, `mem_degreeLE`, `mem_degreeLT`, `monic_geom_sum_X`, `monic_restriction`, `natDegree_restriction`, `not_finite`, `prime_C_iff`, `restriction_one`, `restriction_zero`, `span_le_degreeLE_of_finite`, `span_of_finite_le_degreeLT`, `sup_aeval_range_eq_top_of_isCoprime`, `sup_ker_aeval_eq_ker_aeval_mul_of_coprime`, `sup_ker_aeval_le_ker_aeval_mul`, `support_restriction`, `exists_C_coeff_notMem`, `mem_span_C_coeff`, `span_le_of_C_coeff_mem`	66
Total	75

Ideal

Definitions

Name	Category	Theorems
`degreeLE` 📖	CompOp	1 math math: `is_fg_degreeLE`
`leadingCoeff` 📖	CompOp	1 math math: `mem_leadingCoeff`
`leadingCoeffNth` 📖	CompOp	3 math math: `mem_leadingCoeffNth_zero`, `mem_leadingCoeffNth`, `leadingCoeffNth_mono`
`ofPolynomial` 📖	CompOp	1 math math: `mem_ofPolynomial`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_zero_of_constant_mem_of_maximal` 📖	mathematical	`IsField` `Ring.toSemiring` `Polynomial` `Ideal` `Polynomial.semiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `Polynomial.C`	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`Classical.by_contradiction` `IsMaximal.ne_top` `eq_top_iff_one` `IsField.mul_inv_cancel` `RingHom.map_mul` `IsField.mul_comm` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `mul_mem_left`
`isPrime_map_C_iff_isPrime` 📖	mathematical	—	`IsPrime` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	`RingHom.instRingHomClass` `comap_isPrime` `ext` `Polynomial.coeff_C_zero` `Polynomial.coeff_C_ne_zero` `eq_top_iff_one` `mem_map_C_iff` `Polynomial.coeff_one_zero` `IsPrime.ne_top'` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `Polynomial.coeff_mul` `Finset.insert_erase` `Finset.HasAntidiagonal.mem_antidiagonal` `Finset.sum_insert` `Finset.notMem_erase` `Iff.not` `add_mem_iff_left` `Submodule.sum_mem` `Finset.mem_erase` `mul_comm` `mul_mem_left` `Nat.find_min` `IsPrime.mem_or_mem'` `Nat.find_spec`
`isPrime_map_C_of_isPrime` 📖	mathematical	—	`IsPrime` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `map` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	`isPrime_map_C_iff_isPrime`
`is_fg_degreeLE` 📖	mathematical	—	`Submodule.FG` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `Polynomial.module` `Semiring.toModule` `degreeLE` `WithBot` `WithBot.natCast`	—	`isNoetherian_submodule_left` `isNoetherian_of_fg_of_noetherian` `Polynomial.degreeLE_eq_span_X_pow`
`leadingCoeffNth_mono` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `leadingCoeffNth`	—	`mul_mem_right` `instIsTwoSided` `le_trans` `Polynomial.degree_mul_le` `le_imp_le_of_le_of_le` `add_le_add_left` `WithBot.addRightMono` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `le_refl` `add_le_add_right` `WithBot.addLeftMono` `Polynomial.degree_X_pow_le` `Nat.cast_add` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `Polynomial.leadingCoeff_mul_X_pow`
`mem_leadingCoeff` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `leadingCoeff` `Polynomial` `Polynomial.semiring` `Polynomial.leadingCoeff`	—	`leadingCoeff.eq_1` `Submodule.mem_iSup_of_directed` `leadingCoeffNth_mono` `Polynomial.degree_le_natDegree`
`mem_leadingCoeffNth` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `leadingCoeffNth` `Polynomial` `Polynomial.semiring` `WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `WithBot.natCast` `Polynomial.leadingCoeff`	—	`RingHomSurjective.ids` `lt_or_eq_of_le` `zero_mem` `bot_le` `Polynomial.leadingCoeff_zero` `Polynomial.coeff_eq_zero_of_degree_lt` `le_of_eq` `Polynomial.leadingCoeff.eq_1` `Polynomial.natDegree.eq_1` `Nat.cast_withBot` `WithBot.unbotD_coe` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `Polynomial.natDegree_le_of_degree_le` `le_trans` `Polynomial.degree_mul_le` `add_le_add` `WithBot.addLeftMono` `WithBot.addRightMono` `covariant_swap_add_of_covariant_add` `Polynomial.degree_le_natDegree` `Polynomial.degree_X_pow_le` `Nat.cast_add` `le_refl` `mul_mem_right` `instIsTwoSided` `Polynomial.coeff_mul_X_pow`
`mem_leadingCoeffNth_zero` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `leadingCoeffNth` `Polynomial` `Polynomial.semiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `Polynomial.C`	—	`mem_leadingCoeffNth` `Polynomial.leadingCoeff.eq_1` `Polynomial.natDegree_le_of_degree_le` `Polynomial.eq_C_of_degree_le_zero` `Polynomial.degree_C_le` `Polynomial.leadingCoeff_C`
`mem_map_C_iff` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `Ideal` `Polynomial.semiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `map` `RingHom` `RingHom.instFunLike` `Polynomial.C` `Polynomial.coeff`	—	`Submodule.span_induction` `Set.mem_image` `Polynomial.coeff_C` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `Polynomial.coeff_add` `add_mem` `smul_eq_mul` `Polynomial.coeff_mul` `Submodule.sum_mem` `mul_mem_left` `Polynomial.sum_monomial_eq` `mul_comm` `mem_map_of_mem`
`mem_ofPolynomial` 📖	mathematical	—	`Polynomial` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `Polynomial.module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `ofPolynomial` `Ideal`	—	—
`polynomial_mem_ideal_of_coeff_mem_ideal` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `comap` `Polynomial` `RingHom` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `RingHom.instRingHomClass` `Polynomial.coeff`	`Polynomial` `CommSemiring.toSemiring` `Ideal` `Polynomial.semiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`RingHom.instRingHomClass` `Submodule.sum_mem` `mul_mem_right` `instIsTwoSided` `Polynomial.sum_C_mul_X_pow_eq`
`polynomial_not_isField` 📖	mathematical	—	`IsField` `Polynomial` `Ring.toSemiring` `Polynomial.semiring`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Unique.instSubsingleton` `IsField.mul_inv_cancel` `Polynomial.X_ne_zero` `right_ne_zero_of_mul_eq_one` `Polynomial.nontrivial` `Polynomial.degree_lt_degree_mul_X` `Polynomial.degree_eq_bot` `Nat.WithBot.lt_zero_iff` `Polynomial.degree_one` `Polynomial.X_mul`

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aeval_natDegree_le` 📖	mathematical	`totalDegree` `Polynomial.natDegree` `CommSemiring.toSemiring`	`Polynomial.natDegree` `CommSemiring.toSemiring` `DFunLike.coe` `AlgHom` `MvPolynomial` `Polynomial` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `Polynomial.commSemiring` `AddMonoidAlgebra.algebra` `Algebra.id` `Polynomial.algebraOfAlgebra` `AlgHom.funLike` `aeval`	—	`aeval_def` `eval₂.eq_1` `LE.le.trans` `Polynomial.natDegree_sum_le` `Finset.sup_le` `Polynomial.natDegree_C_mul_le` `Polynomial.natDegree_prod_le` `Finset.sum_mul` `mul_le_mul'` `Nat.instMulLeftMono` `covariant_swap_mul_of_covariant_mul` `totalDegree.eq_1` `Finset.le_sup_of_le` `le_rfl` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Polynomial.natDegree_pow_le`
`instFiniteOfIsEmpty` 📖	mathematical	—	`Module.Finite` `MvPolynomial` `CommSemiring.toSemiring` `AddMonoidAlgebra.addAddCommMonoid` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `AddMonoidAlgebra.module` `Semiring.toModule`	—	`Module.Finite.equiv` `Module.Finite.self` `RingHomInvPair.ids`
`isNoetherianRing` 📖	mathematical	—	`IsNoetherianRing` `MvPolynomial` `CommRing.toCommSemiring` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid`	—	`nonempty_fintype` `isNoetherianRing_of_ringEquiv` `isNoetherianRing_fin`
`isNoetherianRing_fin` 📖	mathematical	—	`IsNoetherianRing` `MvPolynomial` `CommRing.toCommSemiring` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid`	—	`isNoetherianRing_fin_0` `isNoetherianRing_of_ringEquiv` `Polynomial.isNoetherianRing`
`isNoetherianRing_fin_0` 📖	mathematical	—	`IsNoetherianRing` `MvPolynomial` `CommRing.toCommSemiring` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid`	—	`isNoetherianRing_of_ringEquiv` `Fin.isEmpty'`
`ker_map` 📖	mathematical	—	`RingHom.ker` `MvPolynomial` `CommRing.toCommSemiring` `RingHom` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddMonoidAlgebra.semiring` `Finsupp.instAddMonoid` `RingHom.instFunLike` `RingHom.instRingHomClass` `map` `Ideal.map` `Semiring.toNonAssocSemiring` `C`	—	`Ideal.ext` `RingHom.instRingHomClass` `mem_map_C_iff` `RingHom.mem_ker` `ext_iff` `coeff_map`
`ker_mapAlgHom` 📖	mathematical	—	`RingHom.ker` `MvPolynomial` `CommRing.toCommSemiring` `AlgHom` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `AlgHom.funLike` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `mapAlgHom` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `RingHom.instFunLike` `C`	—	`ker_map`
`map_mvPolynomial_eq_eval₂` 📖	mathematical	—	`DFunLike.coe` `RingHom` `MvPolynomial` `CommRing.toCommSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `eval₂` `RingHom.comp` `C` `X`	—	`nonempty_fintype` `as_sum` `eval₂_eq'` `map_sum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `monomial_eq` `Finsupp.prod_pow` `RingHom.map_mul` `map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Finset.prod_congr` `RingHom.map_pow` `RingHom.comp_apply`
`mem_ideal_of_coeff_mem_ideal` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.comap` `MvPolynomial` `RingHom` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddMonoidAlgebra.semiring` `Finsupp.instAddMonoid` `RingHom.instFunLike` `C` `RingHom.instRingHomClass` `coeff`	`MvPolynomial` `CommRing.toCommSemiring` `Ideal` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`RingHom.instRingHomClass` `as_sum` `mul_one` `C_mul_monomial` `Ideal.mul_mem_right` `Ideal.instIsTwoSided_1` `Submodule.sum_mem`
`mem_map_C_iff` 📖	mathematical	—	`MvPolynomial` `CommRing.toCommSemiring` `Ideal` `AddMonoidAlgebra.semiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.map` `RingHom` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `RingHom.instFunLike` `C` `coeff`	—	`Submodule.span_induction` `Set.mem_image` `coeff_C` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `coeff_add` `Ideal.add_mem` `smul_eq_mul` `coeff_mul` `Submodule.sum_mem` `Ideal.mul_mem_left` `as_sum` `mul_one` `C_mul_monomial` `Ideal.mem_map_of_mem` `Ideal.mul_mem_right` `Ideal.instIsTwoSided_1`
`prime_C_iff` 📖	mathematical	—	`Prime` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `AddMonoidAlgebra.commSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `RingHom.instFunLike` `C`	—	`comap_prime` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `constantCoeff_C` `C_0` `IsUnit.map` `MonoidWithZeroHomClass.toMonoidHomClass` `exists_finset_rename₂` `Subtype.val_injective` `algHom_C` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `killCompl_rename_app` `map_dvd` `algebraMap_eq` `rename_C` `Finite.of_fintype`
`prime_rename_iff` 📖	mathematical	—	`Prime` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `AddMonoidAlgebra.commSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Finsupp.instAddCommMonoid` `Nat.instAddCommMonoid` `DFunLike.coe` `AlgHom` `Set` `Set.instMembership` `AddMonoidAlgebra.semiring` `CommSemiring.toSemiring` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.algebra` `Algebra.id` `AlgHom.funLike` `rename` `Set.Elem`	—	`ringHom_ext` `rename_C` `iterToSum_C_C` `rename_X` `iterToSum_C_X` `MulEquiv.prime_iff` `RingEquivClass.toMulEquivClass` `AlgEquivClass.toRingEquivClass` `AlgEquiv.instAlgEquivClass` `prime_C_iff`

Polynomial

Definitions

Name	Category	Theorems
`degreeLE` 📖	CompOp	6 math math: `Sequence.span_degreeLE`, `degreeLT_succ_eq_degreeLE`, `span_le_degreeLE_of_finite`, `degreeLE_mono`, `mem_degreeLE`, `degreeLE_eq_span_X_pow`
`degreeLT` 📖	CompOp	39 math math: `degreeLT.addLinearEquiv_symm_apply_inr`, `degreeLT.instFreeSubtypeMemSubmodule`, `toMatrix_sylvesterMap'`, `degreeLT_mono`, `degreeLT.basis_val`, `FirstOrder.Field.lift_genericMonicPoly`, `degreeLT.addLinearEquiv_castAdd`, `degreeLT.addLinearEquiv_apply_fst`, `comap_taylorEquiv_degreeLT`, `degreeLT.addLinearEquiv_apply_snd`, `adjSylvester_comp_sylveserMap`, `degreeLT.instFiniteSubtypeMemSubmodule`, `det_taylorLinearEquiv_toLinearMap`, `degreeLT.addLinearEquiv_apply`, `degreeLT.addLinearEquiv_apply'`, `degreeLT_succ_eq_degreeLE`, `degreeLT.addLinearEquiv_symm_apply_inl`, `degreeLT.addLinearEquiv_symm_apply_inr_basis`, `span_of_finite_le_degreeLT`, `degreeLT.addLinearEquiv_symm_apply`, `degreeLT.addLinearEquiv_symm_apply'`, `eval_eq_sum_degreeLTEquiv`, `det_taylorLinearEquiv`, `degreeLT_eq_span_X_pow`, `toMatrix_sylvesterMap`, `sylvesterMap_apply_coe`, `degreeLT.addLinearEquiv_natAdd`, `taylorLinearEquiv_symm`, `degreeLT.addLinearEquiv_symm_apply_inl_basis`, `taylor_mem_degreeLT`, `degreeLT.basisProd_natAdd`, `degreeLTEquiv_eq_zero_iff_eq_zero`, `sylveserMap_comp_adjSylvester`, `degreeLT.basisProd_castAdd`, `Sequence.span_degreeLT`, `taylorLinearEquiv_apply_coe`, `mem_degreeLT`, `degreeLT.basis_repr`, `map_taylorEquiv_degreeLT`
`degreeLTEquiv` 📖	CompOp	3 math math: `FirstOrder.Field.lift_genericMonicPoly`, `eval_eq_sum_degreeLTEquiv`, `degreeLTEquiv_eq_zero_iff_eq_zero`
`monicEquivDegreeLT` 📖	CompOp	1 math math: `FirstOrder.Field.lift_genericMonicPoly`
`restriction` 📖	CompOp	10 math math: `monic_restriction`, `eval₂_restriction`, `restriction_one`, `degree_restriction`, `restriction_zero`, `map_restriction`, `coeff_restriction`, `natDegree_restriction`, `coeff_restriction'`, `support_restriction`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_prod_mem_ideal_pow_tsub` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `coeff`	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `Finset.sum` `Nat.instAddCommMonoid` `coeff` `Finset.prod` `Polynomial` `CommSemiring.toCommMonoid` `commSemiring`	—	`IsScalarTower.right` `Finset.induction` `Finset.sum_empty` `Finset.prod_empty` `coeff_one` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero` `Ideal.one_eq_top` `Submodule.mem_top` `Finset.sum_insert` `Finset.prod_insert` `coeff_mul` `sum_mem` `Submodule.addSubmonoidClass` `Ideal.pow_le_pow_right` `add_tsub_add_le_tsub_add_tsub` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsScalarTower.left` `pow_add` `Ideal.mul_mem_mul` `Finset.HasAntidiagonal.mem_antidiagonal`
`coeff_restriction` 📖	mathematical	—	`Subring` `Ring.toNonAssocRing` `SetLike.instMembership` `Subring.instSetLike` `Subring.closure` `SetLike.coe` `Finset` `Finset.instSetLike` `coeffs` `Ring.toSemiring` `coeff` `Subring.toRing` `restriction`	—	`finset_sum_coeff` `Finset.sum_congr` `coeff_monomial` `Finset.sum_ite_eq'`
`coeff_restriction'` 📖	mathematical	—	`Subring` `Ring.toNonAssocRing` `SetLike.instMembership` `Subring.instSetLike` `Subring.closure` `SetLike.coe` `Finset` `Finset.instSetLike` `coeffs` `Ring.toSemiring` `coeff` `Subring.toRing` `restriction`	—	`coeff_restriction`
`degreeLE_eq_span_X_pow` 📖	mathematical	—	`degreeLE` `WithBot` `WithBot.natCast` `Submodule.span` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `semiring` `module` `Semiring.toModule` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.image` `instDecidableEq` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `Finset.range`	—	`le_antisymm` `mem_degreeLE` `sum_monomial_eq` `sum.eq_1` `Submodule.sum_mem` `WithBot.coe_le_coe` `Finset.sup_le_iff` `C_mul_X_pow_eq_monomial` `C_mul'` `Submodule.smul_mem` `Submodule.subset_span` `Finset.mem_coe` `Finset.mem_image` `Finset.mem_range` `Submodule.span_le` `Finset.coe_image` `Set.image_subset_iff` `LE.le.trans` `degree_X_pow_le`
`degreeLE_mono` 📖	mathematical	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder`	`Submodule` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `semiring` `module` `Semiring.toModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `degreeLE`	—	`mem_degreeLE` `le_trans`
`degreeLTEquiv_eq_zero_iff_eq_zero` 📖	mathematical	`Polynomial` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `semiring` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `degreeLT`	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Polynomial` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `degreeLT` `Submodule.addCommMonoid` `Pi.addCommMonoid` `Submodule.module` `Pi.Function.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `degreeLTEquiv` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `instZero`	—	`RingHomInvPair.ids` `EquivLike.toEmbeddingLike` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass`
`degreeLT_eq_span_X_pow` 📖	mathematical	—	`degreeLT` `Submodule.span` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `semiring` `module` `Semiring.toModule` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.image` `instDecidableEq` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `Finset.range`	—	`le_antisymm` `mem_degreeLT` `sum_monomial_eq` `sum.eq_1` `Submodule.sum_mem` `WithBot.coe_lt_coe` `Finset.sup_lt_iff` `WithBot.bot_lt_coe` `C_mul_X_pow_eq_monomial` `C_mul'` `Submodule.smul_mem` `Submodule.subset_span` `Submodule.span_le` `Finset.coe_image` `Set.image_subset_iff` `lt_of_le_of_lt` `degree_X_pow_le` `Finset.mem_range`
`degreeLT_mono` 📖	mathematical	—	`Submodule` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `semiring` `module` `Semiring.toModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `degreeLT`	—	`mem_degreeLT` `lt_of_lt_of_le` `WithBot.coe_le_coe`
`degreeLT_succ_eq_degreeLE` 📖	mathematical	—	`degreeLT` `degreeLE` `WithBot` `WithBot.natCast`	—	`Submodule.ext` `mem_degreeLT` `mem_degreeLE` `natDegree_lt_iff_degree_lt` `natDegree_le_iff_degree_le`
`degree_restriction` 📖	mathematical	—	`degree` `Subring` `Ring.toNonAssocRing` `SetLike.instMembership` `Subring.instSetLike` `Subring.closure` `SetLike.coe` `Finset` `Finset.instSetLike` `coeffs` `Ring.toSemiring` `Subring.toRing` `restriction`	—	`support_restriction`
`disjoint_ker_aeval_of_isCoprime` 📖	mathematical	`IsCoprime` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commSemiring`	`Disjoint` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `Submodule.instOrderBot` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `LinearMap` `semiring` `Module.End.instSemiring` `algebraOfAlgebra` `Algebra.id` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.funLike` `aeval`	—	`smulCommClass_self` `IsScalarTower.left` `disjoint_iff_inf_le` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `LinearMap.mem_ker` `Submodule.mem_inf` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `add_zero`
`eval_eq_sum_degreeLTEquiv` 📖	mathematical	`Polynomial` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `semiring` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `degreeLT`	`eval` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.univ` `Fin.fintype` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Polynomial` `Submodule` `semiring` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `degreeLT` `Submodule.addCommMonoid` `Pi.addCommMonoid` `Submodule.module` `Pi.Function.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `degreeLTEquiv` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`RingHomInvPair.ids` `eval_eq_sum` `sum_fin` `MulZeroClass.zero_mul` `mem_degreeLT`
`eval₂_restriction` 📖	mathematical	—	`eval₂` `Ring.toSemiring` `Subring` `Ring.toNonAssocRing` `SetLike.instMembership` `Subring.instSetLike` `Subring.closure` `SetLike.coe` `Finset` `Finset.instSetLike` `coeffs` `Subring.toRing` `RingHom.comp` `Semiring.toNonAssocSemiring` `Subring.subtype` `restriction`	—	`eval₂_eq_sum` `Finset.sum_congr` `coeff_restriction` `support_restriction`
`exists_degree_le_of_mem_span` 📖	mathematical	`Set.Nonempty` `Polynomial` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `semiring` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `Submodule.span`	`Polynomial` `Set` `Set.instMembership` `WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `degree`	—	`not_lt_bot` `degree_zero` `Mathlib.Tactic.Push.not_and_eq` `Submodule.span_le` `SetLike.mem_coe` `mem_degreeLT` `Nat.cast_withBot` `lt_of_lt_of_le` `degree_le_natDegree` `lt_self_iff_false` `degree_eq_natDegree`
`exists_degree_le_of_mem_span_of_finite` 📖	mathematical	`Set.Nonempty` `Polynomial`	`Polynomial` `Set` `Set.instMembership` `WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `degree`	—	`Set.Finite.exists_maximalFor` `instIsTransLe` `exists_degree_le_of_mem_span` `LE.le.trans` `not_lt` `not_lt_iff_le_imp_ge`
`geom_sum_X_comp_X_add_one_eq_sum` 📖	mathematical	—	`comp` `Finset.sum` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `semiring` `Finset.range` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X` `instAdd` `instOne` `instMul` `instNatCast` `Nat.choose`	—	`ext` `zero_comp` `Nat.cast_zero` `geom_sum_succ'` `add_comp` `X_pow_comp` `coeff_add` `coeff_X_add_one_pow` `Nat.cast_add` `Finset.sum_congr` `finset_sum_coeff` `coeff_C_mul_X_pow` `Finset.sum_eq_single` `Nat.choose_eq_zero_of_lt`
`instCharP` 📖	mathematical	—	`CharP` `Polynomial` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `semiring`	—	`map_natCast` `RingHom.instRingHomClass` `C_0`
`instExpChar` 📖	mathematical	—	`ExpChar` `Polynomial` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `semiring`	—	`charZero` `instCharP`
`isNoetherianRing` 📖	mathematical	—	`IsNoetherianRing` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semiring`	—	`isNoetherianRing_iff` `IsNoetherian.wf` `WellFounded.min_mem` `Ideal.is_fg_degreeLE` `le_or_gt` `Ideal.leadingCoeffNth_mono` `Classical.by_contradiction` `WellFounded.not_lt_min` `le_of_lt` `Submodule.span_induction` `Ideal.subset_span` `Ideal.zero_mem` `Ideal.add_mem` `Ideal.mul_mem_left` `C_mul'` `le_antisymm` `Ideal.span_le` `Submodule.subset_span` `Nat.strong_induction_on` `mem_degreeLE` `le_trans` `degree_le_natDegree` `WithBot.coe_le_coe` `ext` `mul_one` `MulZeroClass.mul_zero` `Ideal.mem_leadingCoeffNth` `leadingCoeff_eq_zero` `degree_mul'` `leadingCoeff_X_pow` `degree_X_pow` `degree_eq_natDegree` `Nat.cast_add` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `natDegree_le_of_degree_le` `leadingCoeff_mul_X_pow` `degree_sub_lt` `sub_add_cancel` `Nat.cast_lt` `WithBot.addLeftMono` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero` `Ideal.sub_mem` `Ideal.mul_mem_right` `Ideal.instIsTwoSided_1`
`ker_mapRingHom` 📖	mathematical	—	`RingHom.ker` `Polynomial` `CommSemiring.toSemiring` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `mapRingHom` `Ideal.map` `C`	—	`Ideal.ext` `RingHom.instRingHomClass` `Ideal.mem_map_C_iff` `ext_iff` `coeff_map`
`linearIndependent_powers_iff_aeval` 📖	mathematical	—	`LinearIndependent` `DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `Monoid.toPow` `Module.End.instMonoid` `Polynomial` `instZero`	—	`smulCommClass_self` `IsScalarTower.left` `linearIndependent_iff` `aeval_endomorphism`
`map_restriction` 📖	mathematical	—	`map` `Subring` `Ring.toNonAssocRing` `CommRing.toRing` `SetLike.instMembership` `Subring.instSetLike` `Subring.closure` `SetLike.coe` `Finset` `Finset.instSetLike` `coeffs` `Ring.toSemiring` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `CommRing.toCommSemiring` `SubringClass.toSubsemiringClass` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Subring.instSubringClass` `algebraMap` `Algebra.ofSubring` `Algebra.id` `restriction`	—	`ext` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `coeff_map` `Algebra.algebraMap_ofSubsemiring_apply` `coeff_restriction`
`mem_degreeLE` 📖	mathematical	—	`Polynomial` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `semiring` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `degreeLE` `WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `degree`	—	—
`mem_degreeLT` 📖	mathematical	—	`Polynomial` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `semiring` `module` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `degreeLT` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `degree` `WithBot.natCast`	—	`iInf_congr_Prop` `degree_lt_iff_coeff_zero`
`monic_geom_sum_X` 📖	mathematical	—	`Monic` `Finset.sum` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `semiring` `Finset.range` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Monic.geom_sum` `monic_X` `natDegree_X` `Nat.instZeroLEOneClass`
`monic_restriction` 📖	mathematical	—	`Monic` `Subring` `Ring.toNonAssocRing` `SetLike.instMembership` `Subring.instSetLike` `Subring.closure` `SetLike.coe` `Finset` `Finset.instSetLike` `coeffs` `Ring.toSemiring` `Subring.toRing` `restriction`	—	`natDegree_restriction` `coeff_restriction` `OneMemClass.coe_one` `Subtype.coe_injective`
`natDegree_restriction` 📖	mathematical	—	`natDegree` `Subring` `Ring.toNonAssocRing` `SetLike.instMembership` `Subring.instSetLike` `Subring.closure` `SetLike.coe` `Finset` `Finset.instSetLike` `coeffs` `Ring.toSemiring` `Subring.toRing` `restriction`	—	`degree_restriction`
`not_finite` 📖	mathematical	—	`Module.Finite` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `semiring` `module` `Semiring.toModule`	—	`Module.finite_def` `Submodule.fg_def` `Mathlib.Tactic.Push.not_and_eq` `span_le_degreeLE_of_finite` `Submodule.mem_top` `one_ne_zero` `nonpos_iff_eq_zero` `Nat.instCanonicallyOrderedAdd` `add_le_iff_nonpos_right` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `Nat.cast_le` `WithBot.addLeftMono` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero` `degree_X_pow` `mem_degreeLE`
`prime_C_iff` 📖	mathematical	—	`Prime` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `commSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`comap_prime` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `eval_C` `Ideal.span_singleton_prime` `C_eq_zero` `Set.image_singleton` `Ideal.map_span` `Ideal.isPrime_map_C_of_isPrime`
`restriction_one` 📖	mathematical	—	`restriction` `Polynomial` `Ring.toSemiring` `instOne` `Subring` `Ring.toNonAssocRing` `SetLike.instMembership` `Subring.instSetLike` `Subring.closure` `SetLike.coe` `Finset` `Finset.instSetLike` `coeffs` `Subring.toRing`	—	`ext` `coeff_restriction'` `coeff_one`
`restriction_zero` 📖	mathematical	—	`restriction` `Polynomial` `Ring.toSemiring` `instZero` `Subring` `Ring.toNonAssocRing` `SetLike.instMembership` `Subring.instSetLike` `Subring.closure` `SetLike.coe` `Finset` `Finset.instSetLike` `coeffs` `Subring.toRing`	—	—
`span_le_degreeLE_of_finite` 📖	mathematical	—	`Submodule` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `semiring` `module` `Semiring.toModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.span` `degreeLE` `WithBot` `WithBot.natCast`	—	`exists_degree_le_of_mem_span_of_finite` `mem_degreeLE` `LE.le.trans` `degree_le_natDegree` `Set.not_nonempty_iff_eq_empty` `Submodule.span_empty` `bot_le`
`span_of_finite_le_degreeLT` 📖	mathematical	—	`Submodule` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `semiring` `module` `Semiring.toModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Submodule.span` `degreeLT`	—	`span_le_degreeLE_of_finite` `degreeLT_succ_eq_degreeLE`
`sup_aeval_range_eq_top_of_isCoprime` 📖	mathematical	`IsCoprime` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commSemiring`	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `DFunLike.coe` `AlgHom` `Polynomial` `LinearMap` `semiring` `Module.End.instSemiring` `algebraOfAlgebra` `Algebra.id` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.funLike` `aeval` `Top.top` `Submodule.instTop`	—	`RingHomSurjective.ids` `smulCommClass_self` `IsScalarTower.left` `eq_top_iff` `Submodule.mem_sup` `LinearMap.mem_range` `aeval_mul` `mul_comm` `aeval_add` `aeval_one`
`sup_ker_aeval_eq_ker_aeval_mul_of_coprime` 📖	mathematical	`IsCoprime` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commSemiring`	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `LinearMap` `semiring` `Module.End.instSemiring` `algebraOfAlgebra` `Algebra.id` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.funLike` `aeval` `instMul`	—	`le_antisymm` `smulCommClass_self` `IsScalarTower.left` `sup_ker_aeval_le_ker_aeval_mul` `Submodule.mem_sup` `mul_comm` `mul_assoc` `aeval_mul` `Module.End.mul_apply` `LinearMap.mem_ker` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `add_comm` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `aeval_one`
`sup_ker_aeval_le_ker_aeval_mul` 📖	mathematical	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `LinearMap` `semiring` `Module.End.instSemiring` `algebraOfAlgebra` `Algebra.id` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.funLike` `aeval` `instMul`	—	`smulCommClass_self` `IsScalarTower.left` `Submodule.mem_sup` `mul_comm` `aeval_mul` `Module.End.mul_apply` `LinearMap.mem_ker` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_add` `SemilinearMapClass.toAddHomClass` `add_zero`
`support_restriction` 📖	mathematical	—	`support` `Subring` `Ring.toNonAssocRing` `SetLike.instMembership` `Subring.instSetLike` `Subring.closure` `SetLike.coe` `Finset` `Finset.instSetLike` `coeffs` `Ring.toSemiring` `Subring.toRing` `restriction`	—	`Finset.ext` `coeff_restriction` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `ZeroMemClass.coe_zero` `Subtype.coe_injective`

Polynomial.Monic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`geom_sum` 📖	mathematical	`Polynomial.Monic` `Polynomial.natDegree`	`Polynomial.Monic` `Finset.sum` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `Finset.range` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `geom_sum_succ'` `add_of_left` `pow` `lt_of_le_of_lt` `Polynomial.degree_sum_le` `Finset.sup_lt_iff` `bot_lt_iff_ne_bot` `Polynomial.degree_eq_bot` `ne_zero` `Polynomial.degree_eq_natDegree` `natDegree_pow` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero` `nsmul_lt_nsmul_left` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid`
`geom_sum'` 📖	mathematical	`Polynomial.Monic` `WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Polynomial.degree`	`Polynomial.Monic` `Finset.sum` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `Finset.range` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`geom_sum` `Polynomial.natDegree_pos_iff_degree_pos`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_C_coeff_notMem` 📖	mathematical	`Polynomial` `Ideal` `Polynomial.semiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Polynomial` `Ideal` `Polynomial.semiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `Polynomial.C` `Polynomial.coeff`	—	`Not.imp_symm` `span_le_of_C_coeff_mem` `mem_span_C_coeff`
`mem_span_C_coeff` 📖	mathematical	—	`Polynomial` `Ideal` `Polynomial.semiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.span` `setOf` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `Polynomial.C` `Polynomial.coeff`	—	`Polynomial.sum_C_mul_X_pow_eq` `Submodule.sum_mem` `Submodule.subset_span` `Set.mem_setOf_eq` `Submodule.smul_mem` `Polynomial.monomial_mul_C` `one_mul` `Polynomial.C_mul_X_pow_eq_monomial`
`span_le_of_C_coeff_mem` 📖	mathematical	`Polynomial` `Ideal` `Polynomial.semiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `Polynomial.C` `Polynomial.coeff`	`Ideal` `Polynomial` `Polynomial.semiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.span` `setOf` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `Polynomial.C` `Polynomial.coeff`	—	`Ideal.span_le` `Set.range_subset_iff`

---

← Back to Index