ScaleRoots

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

Statistics

Metric	Count
Definitions `scaleRoots`	1
Theorems `scaleRoots`, `scaleRoots`, `scaleRoots_dvd_iff`, `scaleRoots`, `scaleRoots`, `X_add_C_scaleRoots`, `X_sub_C_scaleRoots`, `add_scaleRoots_of_natDegree_eq`, `coeff_scaleRoots`, `coeff_scaleRoots_natDegree`, `degree_scaleRoots`, `isCoprime_scaleRoots`, `leadingCoeff_scaleRoots`, `map_scaleRoots`, `monic_scaleRoots_iff`, `mul_scaleRoots`, `mul_scaleRoots'`, `mul_scaleRoots_of_noZeroDivisors`, `natDegree_scaleRoots`, `one_scaleRoots`, `pow_scaleRoots'`, `pow_scaleRoots_of_isReduced`, `rootMultiplicity_scaleRoots`, `roots_scaleRoots`, `scaleRoots_C`, `scaleRoots_aeval_eq_zero`, `scaleRoots_aeval_eq_zero_of_aeval_div_eq_zero`, `scaleRoots_dvd`, `scaleRoots_dvd'`, `scaleRoots_dvd_iff`, `scaleRoots_eval_mul`, `scaleRoots_eval₂_eq_zero`, `scaleRoots_eval₂_eq_zero_of_eval₂_div_eq_zero`, `scaleRoots_eval₂_mul`, `scaleRoots_eval₂_mul_of_commute`, `scaleRoots_mul`, `scaleRoots_ne_zero`, `scaleRoots_one`, `scaleRoots_zero`, `support_scaleRoots_eq`, `support_scaleRoots_le`, `zero_scaleRoots`	42
Total	43

Dvd.dvd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`scaleRoots` 📖	mathematical	`Polynomial` `CommSemiring.toSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `Polynomial.commSemiring`	`Polynomial.scaleRoots`	—	`Polynomial.scaleRoots_dvd`

IsCoprime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`scaleRoots` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `IsCoprime` `Polynomial` `Polynomial.commSemiring`	`Polynomial.scaleRoots`	—	`Polynomial.isCoprime_scaleRoots`

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`scaleRoots_dvd_iff` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`Polynomial` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `Polynomial.commSemiring` `Polynomial.scaleRoots`	—	`Polynomial.scaleRoots_dvd_iff`

Polynomial

Definitions

Name	Category	Theorems
`scaleRoots` 📖	CompOp	50 math math: `degree_scaleRoots`, `roots_scaleRoots`, `rootMultiplicity_scaleRoots`, `scaleRoots.isWeaklyEisensteinAt`, `scaleRoots_dvd'`, `scaleRoots_eval₂_mul`, `num_isRoot_scaleRoots_of_aeval_eq_zero`, `isCoprime_scaleRoots`, `one_scaleRoots`, `leadingCoeff_smul_integralNormalization`, `scaleRoots_mul`, `scaleRoots_eval₂_eq_zero`, `support_scaleRoots_eq`, `scaleRoots_eval₂_mul_of_commute`, `mul_scaleRoots_of_noZeroDivisors`, `X_add_C_scaleRoots`, `IsUnit.scaleRoots_dvd_iff`, `scaleRoots_dvd`, `scaleRoots_eval₂_eq_zero_of_eval₂_div_eq_zero`, `coeff_scaleRoots`, `natDegree_scaleRoots`, `scaleRoots_aeval_eq_zero`, `resultant_scaleRoots`, `Factors.scaleRoots`, `pow_scaleRoots_of_isReduced`, `mul_scaleRoots`, `IsLocalization.scaleRoots_commonDenom_mem_lifts`, `coeff_scaleRoots_natDegree`, `scaleRoots_aeval_eq_zero_of_aeval_div_eq_zero`, `scaleRoots_dvd_iff`, `scaleRoots_aeval_eq_zero_of_aeval_mk'_eq_zero`, `X_sub_C_scaleRoots`, `integralNormalization_mul_C_leadingCoeff`, `IsIntegrallyClosed.minpoly_smul`, `zero_scaleRoots`, `leadingCoeff_scaleRoots`, `scaleRoots_zero`, `scaleRoots_C`, `support_scaleRoots_le`, `pow_scaleRoots'`, `scaleRoots_eval_mul`, `IsCoprime.scaleRoots`, `scaleRoots_one`, `mul_scaleRoots'`, `map_scaleRoots`, `monic_scaleRoots_iff`, `Dvd.dvd.scaleRoots`, `resultant_integralNormalization`, `Splits.scaleRoots`, `add_scaleRoots_of_natDegree_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`X_add_C_scaleRoots` 📖	mathematical	—	`scaleRoots` `Polynomial` `instAdd` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `Unique.instSubsingleton` `ext` `coeff_scaleRoots` `coeff_add` `coeff_X_zero` `coeff_C_zero` `zero_add` `natDegree_add_C` `natDegree_X` `tsub_zero` `Nat.instOrderedSub` `pow_one` `mul_coeff_zero` `coeff_X_one` `coeff_C_succ` `add_zero` `tsub_self` `Nat.instCanonicallyOrderedAdd` `pow_zero` `mul_one` `coeff_mul_C` `MulZeroClass.zero_mul` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le`
`X_sub_C_scaleRoots` 📖	mathematical	—	`scaleRoots` `Ring.toSemiring` `Polynomial` `instSub` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `Unique.instSubsingleton` `ext` `coeff_scaleRoots` `coeff_sub` `coeff_X_zero` `coeff_C_zero` `zero_sub` `natDegree_sub_C` `natDegree_X` `tsub_zero` `Nat.instOrderedSub` `pow_one` `neg_mul` `mul_coeff_zero` `zero_add` `coeff_X_one` `coeff_C_succ` `sub_zero` `tsub_self` `Nat.instCanonicallyOrderedAdd` `pow_zero` `mul_one` `coeff_mul_C` `MulZeroClass.zero_mul` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le`
`add_scaleRoots_of_natDegree_eq` 📖	mathematical	`natDegree` `CommSemiring.toSemiring`	`Polynomial` `Algebra.toSMul` `semiring` `algebraOfAlgebra` `Algebra.id` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instAdd` `scaleRoots`	—	`ext` `coeff_smul` `coeff_scaleRoots` `coeff_add` `mul_comm` `Distrib.rightDistribClass` `mul_assoc` `pow_add` `lt_or_ge` `coeff_eq_zero_of_natDegree_lt` `MulZeroClass.zero_mul` `add_comm` `tsub_add_tsub_cancel` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `natDegree_add_le_of_degree_le` `le_rfl` `Eq.ge`
`coeff_scaleRoots` 📖	mathematical	—	`coeff` `scaleRoots` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `natDegree`	—	`finset_sum_coeff` `Finset.sum_congr` `coeff_monomial` `Finset.sum_ite_eq'` `MulZeroClass.zero_mul`
`coeff_scaleRoots_natDegree` 📖	mathematical	—	`coeff` `scaleRoots` `natDegree` `leadingCoeff`	—	`leadingCoeff.eq_1` `coeff_scaleRoots` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero` `mul_one`
`degree_scaleRoots` 📖	mathematical	—	`degree` `scaleRoots`	—	`zero_scaleRoots` `le_antisymm` `Finset.sup_mono` `support_scaleRoots_le` `degree_le_degree` `coeff_scaleRoots_natDegree` `leadingCoeff_eq_zero`
`isCoprime_scaleRoots` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `IsCoprime` `Polynomial` `commSemiring`	`scaleRoots`	—	`natDegree_eq_of_natDegree_add_eq_zero` `natDegree_one` `smul_smul` `smul_mul_assoc` `IsScalarTower.right` `mul_assoc` `IsUnit.val_inv_mul` `one_pow` `mul_one` `add_scaleRoots_of_natDegree_eq` `tsub_zero` `Nat.instOrderedSub` `one_scaleRoots` `one_smul`
`leadingCoeff_scaleRoots` 📖	mathematical	—	`leadingCoeff` `scaleRoots`	—	`leadingCoeff.eq_1` `natDegree_scaleRoots` `coeff_scaleRoots_natDegree`
`map_scaleRoots` 📖	mathematical	—	`map` `scaleRoots` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	—	`ext` `coeff_map` `coeff_scaleRoots` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `natDegree_map_of_leadingCoeff_ne_zero`
`monic_scaleRoots_iff` 📖	mathematical	—	`Monic` `scaleRoots`	—	`leadingCoeff_scaleRoots`
`mul_scaleRoots` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `Algebra.toSMul` `semiring` `algebraOfAlgebra` `Algebra.id` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `natDegree` `instMul` `scaleRoots`	—	`ext` `coeff_smul` `coeff_scaleRoots` `coeff_mul` `lt_or_ge` `coeff_eq_zero_of_natDegree_lt` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `mul_comm` `mul_assoc` `pow_add` `add_comm` `tsub_add_tsub_cancel` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `natDegree_mul_le` `Finset.sum_mul` `Finset.sum_congr` `tsub_add_tsub_comm` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le`
`mul_scaleRoots'` 📖	mathematical	—	`scaleRoots` `CommSemiring.toSemiring` `Polynomial` `instMul`	—	`mul_scaleRoots` `natDegree_mul'` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero` `one_smul`
`mul_scaleRoots_of_noZeroDivisors` 📖	mathematical	—	`scaleRoots` `CommSemiring.toSemiring` `Polynomial` `instMul`	—	`MulZeroClass.zero_mul` `zero_scaleRoots` `MulZeroClass.mul_zero` `mul_scaleRoots'`
`natDegree_scaleRoots` 📖	mathematical	—	`natDegree` `scaleRoots`	—	`degree_scaleRoots`
`one_scaleRoots` 📖	mathematical	—	`scaleRoots` `Polynomial` `instOne`	—	`ext` `coeff_scaleRoots` `natDegree_one` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero` `mul_one`
`pow_scaleRoots'` 📖	mathematical	—	`scaleRoots` `CommSemiring.toSemiring` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring`	—	`pow_zero` `one_scaleRoots` `pow_succ` `mul_scaleRoots'` `leadingCoeff_pow'` `MulZeroClass.zero_mul`
`pow_scaleRoots_of_isReduced` 📖	mathematical	—	`scaleRoots` `CommSemiring.toSemiring` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring`	—	`zero_pow_eq` `one_scaleRoots` `zero_scaleRoots` `pow_zero` `pow_scaleRoots'`
`rootMultiplicity_scaleRoots` 📖	mathematical	`IsLeftRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`rootMultiplicity` `CommRing.toRing` `scaleRoots` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`subsingleton_or_nontrivial` `Unique.instSubsingleton` `zero_scaleRoots` `rootMultiplicity_zero` `eq_or_ne` `exists_eq_pow_rootMultiplicity_mul_and_not_dvd` `Mathlib.Tactic.Contrapose.contrapose₄` `mul_scaleRoots'` `leadingCoeff_pow'` `leadingCoeff_X_sub_C` `one_pow` `NeZero.one` `one_mul` `leadingCoeff_eq_zero` `pow_scaleRoots'` `X_sub_C_scaleRoots` `mul_comm` `rootMultiplicity_mul_X_sub_C_pow` `scaleRoots_ne_zero` `scaleRoots_eval_mul` `IsLeftRegular.mul_left_eq_zero_iff` `IsLeftRegular.pow` `IsRoot.def` `dvd_iff_isRoot`
`roots_scaleRoots` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`roots` `scaleRoots` `Multiset.map` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Multiset.ext'` `IsUnit.isUnit_iff_mulLeft_bijective` `count_roots` `rootMultiplicity_scaleRoots` `IsRegular.left` `IsUnit.isRegular` `Multiset.count_map_eq_count'`
`scaleRoots_C` 📖	mathematical	—	`scaleRoots` `DFunLike.coe` `RingHom` `Polynomial` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`ext` `coeff_scaleRoots` `natDegree_C` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero` `mul_one`
`scaleRoots_aeval_eq_zero` 📖	mathematical	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `RingHom` `RingHom.instFunLike` `algebraMap` `scaleRoots`	—	`aeval_def` `scaleRoots_eval₂_mul_of_commute` `Algebra.commutes` `Commute.eq_1` `SemiconjBy.eq_1` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `mul_comm` `MulZeroClass.mul_zero`
`scaleRoots_aeval_eq_zero_of_aeval_div_eq_zero` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `algebraMap` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	`scaleRoots`	—	`scaleRoots_eval₂_eq_zero_of_eval₂_div_eq_zero`
`scaleRoots_dvd` 📖	mathematical	`Polynomial` `CommSemiring.toSemiring` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `commSemiring`	`scaleRoots`	—	`mul_scaleRoots_of_noZeroDivisors` `dvd_mul_right`
`scaleRoots_dvd'` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Polynomial` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `commSemiring`	`scaleRoots`	—	`IsUnit.dvd_mul_left` `IsUnit.map` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsUnit.pow` `Algebra.smul_def` `mul_scaleRoots` `dvd_mul_right`
`scaleRoots_dvd_iff` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`Polynomial` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `commSemiring` `scaleRoots`	—	`IsUnit.mul_val_inv` `scaleRoots_one` `scaleRoots_dvd'` `Units.isUnit`
`scaleRoots_eval_mul` 📖	mathematical	—	`eval` `CommSemiring.toSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `scaleRoots` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `natDegree`	—	`scaleRoots_eval₂_mul`
`scaleRoots_eval₂_eq_zero` 📖	mathematical	`eval₂` `CommSemiring.toSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `scaleRoots`	—	`scaleRoots_eval₂_mul` `MulZeroClass.mul_zero`
`scaleRoots_eval₂_eq_zero_of_eval₂_div_eq_zero` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.instFunLike` `eval₂` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	`scaleRoots`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Subsingleton.eq_zero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `scaleRoots_zero` `natDegree_of_subsingleton` `pow_zero` `zero_smul` `eval₂_zero` `mul_div_assoc` `mul_comm` `mul_div_cancel_right₀` `EuclideanDomain.toMulDivCancelClass` `map_ne_zero_of_mem_nonZeroDivisors` `scaleRoots_eval₂_eq_zero`
`scaleRoots_eval₂_mul` 📖	mathematical	—	`eval₂` `CommSemiring.toSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `scaleRoots` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `natDegree`	—	`scaleRoots_eval₂_mul_of_commute` `mul_comm`
`scaleRoots_eval₂_mul_of_commute` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike`	`eval₂` `scaleRoots` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `natDegree`	—	`eval₂_eq_sum` `Finset.sum_congr` `coeff_scaleRoots` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Finset.sum_subset` `support_scaleRoots_le` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MulZeroClass.zero_mul` `RingHom.map_mul` `RingHom.map_pow` `pow_add` `Commute.mul_pow` `mul_assoc` `Commute.left_comm` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `le_natDegree_of_ne_zero` `mem_support_iff`
`scaleRoots_mul` 📖	mathematical	—	`scaleRoots` `CommSemiring.toSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`ext` `coeff_scaleRoots` `mul_pow` `natDegree_scaleRoots` `mul_assoc`
`scaleRoots_ne_zero` 📖	—	—	—	—	`leadingCoeff_eq_zero` `coeff_scaleRoots_natDegree`
`scaleRoots_one` 📖	mathematical	—	`scaleRoots` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring`	—	`ext` `coeff_scaleRoots` `one_pow` `mul_one`
`scaleRoots_zero` 📖	mathematical	—	`scaleRoots` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Polynomial` `SMulZeroClass.toSMul` `instZero` `smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `NonUnitalNonAssocSemiring.toDistribSMul` `leadingCoeff` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `X` `natDegree`	—	`ext` `coeff_scaleRoots` `zero_pow_eq` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `coeff_smul` `coeff_X_pow` `coeff_eq_zero_of_natDegree_lt` `lt_of_le_of_ne` `Eq.ge`
`support_scaleRoots_eq` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	`support` `scaleRoots`	—	`le_antisymm` `support_scaleRoots_le` `coeff_scaleRoots` `pow_mem` `Submonoid.instSubmonoidClass`
`support_scaleRoots_le` 📖	mathematical	—	`Finset` `Preorder.toLE` `PartialOrder.toPreorder` `Finset.partialOrder` `support` `scaleRoots`	—	`coeff_scaleRoots` `left_ne_zero_of_mul`
`zero_scaleRoots` 📖	mathematical	—	`scaleRoots` `Polynomial` `instZero`	—	`ext` `coeff_scaleRoots` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero` `mul_one`

Polynomial.Factors

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`scaleRoots` 📖	mathematical	`Polynomial.Splits` `CommSemiring.toSemiring`	`Polynomial.scaleRoots`	—	`Polynomial.Splits.scaleRoots`

Polynomial.Splits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`scaleRoots` 📖	mathematical	`Polynomial.Splits` `CommSemiring.toSemiring`	`Polynomial.scaleRoots`	—	`subsingleton_or_nontrivial` `Unique.instSubsingleton` `eq_or_ne` `Polynomial.zero_scaleRoots` `Polynomial.splits_iff_exists_multiset'` `Polynomial.mul_scaleRoots'` `Polynomial.Monic.leadingCoeff` `Polynomial.monic_multiset_prod_of_monic` `Polynomial.monic_X_add_C` `Polynomial.leadingCoeff_C` `mul_one` `Polynomial.scaleRoots_C` `mul` `C` `Multiset.induction_on` `Polynomial.one_scaleRoots` `Multiset.map_cons` `Multiset.prod_cons` `Polynomial.leadingCoeff_X_add_C` `one_mul` `Polynomial.Monic.ne_zero` `Polynomial.X_add_C_scaleRoots` `X_add_C`

---

← Back to Index