Expand

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

Statistics

Metric	Count
Definitions `contract`, `expand`	2
Theorems `expand`, `coe_expand`, `coeff_contract`, `coeff_expand`, `coeff_expand_mul`, `coeff_expand_mul'`, `contract_C`, `contract_add`, `contract_expand`, `contract_mul_expand`, `contract_one`, `derivative_expand`, `expand_C`, `expand_X`, `expand_aeval`, `expand_char`, `expand_contract`, `expand_contract'`, `expand_eq_C`, `expand_eq_comp_X_pow`, `expand_eq_sum`, `expand_eq_zero`, `expand_eval`, `expand_expand`, `expand_inj`, `expand_injective`, `expand_monomial`, `expand_mul`, `expand_ne_zero`, `expand_one`, `expand_pow`, `expand_zero`, `isCoprime_expand`, `isLocalHom_expand`, `leadingCoeff_expand`, `map_contract`, `map_expand`, `map_expand_pow_char`, `map_frobenius_expand`, `map_iterateFrobenius_expand`, `monic_expand_iff`, `natDegree_expand`, `of_irreducible_expand`, `of_irreducible_expand_pow`, `rootMultiplicity_expand`, `rootMultiplicity_expand_pow`	46
Total	48

Polynomial

Definitions

Name	Category	Theorems
`contract` 📖	CompOp	9 math math: `expand_contract`, `contract_expand`, `map_contract`, `contract_add`, `contract_one`, `contract_C`, `coeff_contract`, `expand_contract'`, `contract_mul_expand`
`expand` 📖	CompOp	66 math math: `roots_expand`, `expand_contract`, `expand_eq_sum`, `contract_expand`, `Irreducible.natSepDegree_eq_one_iff_of_monic'`, `rootMultiplicity_expand_pow`, `derivative_expand`, `Monic.natSepDegree_eq_one_iff_of_irreducible'`, `cyclotomic_expand_eq_cyclotomic_mul`, `rootsExpandPowEquivRoots_apply`, `map_expand`, `expand_eq_comp_X_pow`, `expand_one`, `separable_or`, `rootsExpandEquivRoots_apply`, `expand_C`, `roots_expand_map_frobenius`, `roots_expand_image_frobenius`, `rootsExpandPowToRoots_apply`, `isCoprime_expand`, `expand_inj`, `expand_expand`, `IsPrimitiveRoot.minpoly_dvd_expand`, `roots_expand_image_frobenius_subset`, `expand_eq_zero`, `expand_zero`, `roots_expand_pow_map_iterateFrobenius_le`, `rootMultiplicity_expand`, `expand_X`, `expand_monomial`, `monic_expand_iff`, `natSepDegree_expand`, `roots_expand_pow_map_iterateFrobenius`, `map_expand_pow_char`, `coeff_expand_mul`, `not_irreducible_expand`, `expand_mul`, `polynomial_expand_eq`, `coe_expand`, `coeff_expand`, `rootsExpandToRoots_apply`, `leadingCoeff_expand`, `expand_eq_C`, `expand_contract'`, `ZMod.expand_card`, `exists_separable_of_irreducible`, `roots_expand_image_iterateFrobenius`, `expand_char`, `roots_expand_pow_image_iterateFrobenius_subset`, `expand_eval`, `FiniteField.expand_card`, `coeff_expand_mul'`, `roots_expand_pow`, `contract_mul_expand`, `map_frobenius_expand`, `minpoly.natSepDegree_eq_one_iff_eq_expand_X_sub_C`, `Monic.expand`, `natDegree_expand`, `cyclotomic_expand_eq_cyclotomic`, `expand_aeval`, `isLocalHom_expand`, `matPolyEquiv_eq_X_pow_sub_C`, `roots_expand_map_frobenius_le`, `expand_injective`, `map_iterateFrobenius_expand`, `expand_pow`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_expand` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `eval₂` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	—
`coeff_contract` 📖	mathematical	—	`coeff` `CommSemiring.toSemiring` `contract`	—	`finset_sum_coeff` `Finset.sum_congr` `coeff_monomial` `Finset.sum_ite_eq'` `coeff_eq_zero_of_natDegree_lt` `mul_one` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Ne.bot_lt` `zero_le` `Nat.instCanonicallyOrderedAdd`
`coeff_expand` 📖	mathematical	—	`coeff` `CommSemiring.toSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`expand_eq_sum` `coeff_sum` `C_mul_X_pow_eq_monomial` `coeff_monomial` `Finset.sum_congr` `Finset.sum_eq_single` `notMem_support_iff` `Finset.sum_eq_zero`
`coeff_expand_mul` 📖	mathematical	—	`coeff` `CommSemiring.toSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand`	—	`coeff_expand` `dvd_mul_left`
`coeff_expand_mul'` 📖	mathematical	—	`coeff` `CommSemiring.toSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand`	—	`mul_comm` `coeff_expand_mul`
`contract_C` 📖	mathematical	—	`contract` `DFunLike.coe` `RingHom` `Polynomial` `CommSemiring.toSemiring` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`Finset.sum_congr` `natDegree_C` `zero_add` `Finset.sum_singleton` `MulZeroClass.zero_mul` `coeff_C_zero`
`contract_add` 📖	mathematical	—	`contract` `Polynomial` `CommSemiring.toSemiring` `instAdd`	—	`ext` `coeff_add` `coeff_contract`
`contract_expand` 📖	mathematical	—	`contract` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand`	—	`ext` `coeff_contract` `coeff_expand` `Ne.bot_lt`
`contract_mul_expand` 📖	mathematical	—	`contract` `Polynomial` `CommSemiring.toSemiring` `instMul` `DFunLike.coe` `AlgHom` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand`	—	`ext` `coeff_contract` `coeff_mul` `Finset.sum_subset` `add_mul` `Distrib.rightDistribClass` `dvd_mul_left` `Ne.bot_lt` `mul_comm` `mul_add` `Distrib.leftDistribClass` `coeff_expand` `MulZeroClass.mul_zero` `Finset.sum_image` `Finset.sum_congr` `coeff_expand_mul`
`contract_one` 📖	mathematical	—	`contract`	—	`ext` `coeff_contract` `one_ne_zero` `mul_one`
`derivative_expand` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `derivative` `AlgHom` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `instMul` `instNatCast` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`coe_expand` `derivative_eval₂_C` `derivative_pow` `C_eq_natCast` `derivative_X` `mul_one`
`expand_C` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	—	`eval₂_C`
`expand_X` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `X` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`eval₂_X`
`expand_aeval` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `expand` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`induction_on` `expand_C` `aeval_C` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `aeval_add` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `expand_X` `aeval_X`
`expand_char` 📖	mathematical	—	`map` `CommSemiring.toSemiring` `frobenius` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`map_frobenius_expand`
`expand_contract` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `derivative` `instZero`	`AlgHom` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `contract`	—	`ext` `coeff_expand` `Ne.bot_lt` `coeff_contract` `dvd_zero` `coeff_derivative` `zero_eq_mul` `coeff_zero` `CharP.cast_eq_zero_iff` `Nat.cast_succ`
`expand_contract'` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `derivative` `instZero`	`AlgHom` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `contract`	—	`expand_one` `contract_one` `expand_contract` `Nat.Prime.ne_zero`
`expand_eq_C` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C`	—	`expand_C`
`expand_eq_comp_X_pow` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `comp` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	—
`expand_eq_sum` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMul` `RingHom` `RingHom.instFunLike` `C` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `X`	—	`eval₂_def`
`expand_eq_zero` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `instZero`	—	`expand_injective` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`
`expand_eval` 📖	mathematical	—	`eval` `CommSemiring.toSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`induction_on` `expand_C` `eval_C` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `eval_add` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `expand_X` `eval_mul` `eval_pow` `eval_X`
`expand_expand` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand`	—	`induction_on` `expand_C` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `expand_X` `pow_mul`
`expand_inj` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand`	—	`expand_injective`
`expand_injective` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `DFunLike.coe` `AlgHom` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand`	—	`ext` `coeff_expand_mul`
`expand_monomial` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `module` `LinearMap.instFunLike` `monomial`	—	`map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `expand_X` `mul_comm` `pow_mul`
`expand_mul` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand`	—	`expand_expand`
`expand_ne_zero` 📖	—	—	—	—	`Iff.not` `expand_eq_zero`
`expand_one` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand`	—	`induction_on` `expand_C` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `expand_X` `pow_one`
`expand_pow` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `Monoid.toNatPow` `Nat.instMonoid` `Nat.iterate`	—	`pow_zero` `expand_one` `Function.iterate_zero` `Function.iterate_succ_apply'` `pow_succ'` `expand_mul`
`expand_zero` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `C` `eval` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`pow_zero` `eval₂_at_one`
`isCoprime_expand` 📖	mathematical	—	`IsCoprime` `Polynomial` `CommSemiring.toSemiring` `commSemiring` `DFunLike.coe` `AlgHom` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand`	—	`contract_mul_expand` `contract_add` `contract_C` `IsCoprime.map`
`isLocalHom_expand` 📖	mathematical	—	`IsLocalHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AlgHom` `semiring` `algebraOfAlgebra` `Algebra.id` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.funLike` `expand`	—	`eq_C_of_degree_eq_zero` `degree_eq_zero_of_isUnit` `IsDomain.to_noZeroDivisors` `IsDomain.toNontrivial` `expand_eq_C` `dvd_zero` `coeff_expand` `isUnit_C`
`leadingCoeff_expand` 📖	mathematical	—	`leadingCoeff` `CommSemiring.toSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand`	—	`natDegree_expand` `coeff_expand_mul`
`map_contract` 📖	mathematical	—	`map` `CommSemiring.toSemiring` `contract`	—	`ext` `coeff_map` `coeff_contract`
`map_expand` 📖	mathematical	—	`map` `CommSemiring.toSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand`	—	`expand_zero` `map_C` `eval_one_map` `ext` `coeff_map` `coeff_expand` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`map_expand_pow_char` 📖	mathematical	—	`map` `CommSemiring.toSemiring` `iterateFrobenius` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `Monoid.toNatPow` `Nat.instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`map_iterateFrobenius_expand`
`map_frobenius_expand` 📖	mathematical	—	`map` `CommSemiring.toSemiring` `frobenius` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`induction_on'` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_add` `add_pow_expChar` `instExpChar` `expand_monomial` `map_monomial` `C_mul_X_pow_eq_monomial` `mul_pow` `RingHom.map_pow` `frobenius_def` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero`
`map_iterateFrobenius_expand` 📖	mathematical	—	`map` `CommSemiring.toSemiring` `iterateFrobenius` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `Monoid.toNatPow` `Nat.instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`iterateFrobenius_zero` `pow_zero` `expand_one` `map_id` `pow_one` `pow_succ` `pow_mul` `map_frobenius_expand` `pow_succ'` `iterateFrobenius.congr_simp` `add_comm` `iterateFrobenius_add` `iterateFrobenius_one`
`monic_expand_iff` 📖	mathematical	—	`Monic` `CommSemiring.toSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand`	—	`leadingCoeff_expand`
`natDegree_expand` 📖	mathematical	—	`natDegree` `CommSemiring.toSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand`	—	`coe_expand` `pow_zero` `MulZeroClass.mul_zero` `C_1` `eval₂_hom` `natDegree_C` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `natDegree_zero` `MulZeroClass.zero_mul` `expand_eq_zero` `WithBot.charZero` `Nat.instCharZero` `degree_eq_natDegree` `le_antisymm` `degree_le_iff_coeff_zero` `coeff_expand` `coeff_eq_zero_of_natDegree_lt` `Mathlib.Tactic.Contrapose.contrapose₁` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `le_degree_of_ne_zero` `coeff_expand_mul` `leadingCoeff.eq_1` `leadingCoeff_eq_zero`
`of_irreducible_expand` 📖	—	`Irreducible` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `DFunLike.coe` `AlgHom` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand`	—	—	`isLocalHom_expand` `Ne.bot_lt` `Irreducible.of_map` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`
`of_irreducible_expand_pow` 📖	—	`Irreducible` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `DFunLike.coe` `AlgHom` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `Monoid.toNatPow` `Nat.instMonoid`	—	—	`expand_one` `pow_zero` `of_irreducible_expand` `expand_expand` `pow_succ'`
`rootMultiplicity_expand` 📖	mathematical	—	`rootMultiplicity` `CommRing.toRing` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`pow_one` `rootMultiplicity_expand_pow`
`rootMultiplicity_expand_pow` 📖	mathematical	—	`rootMultiplicity` `CommRing.toRing` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `expand` `Monoid.toNatPow` `Nat.instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`eq_or_ne` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `rootMultiplicity_zero` `MulZeroClass.mul_zero` `exists_eq_pow_rootMultiplicity_mul_and_not_dvd` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `expand_X` `expand_C` `RingHom.instRingHomClass` `sub_pow_expChar_pow` `instExpChar` `pow_mul` `mul_comm` `rootMultiplicity_mul_X_sub_C_pow` `expand_ne_zero` `expChar_pow_pos` `right_ne_zero_of_mul` `rootMultiplicity_eq_zero` `expand_eq_comp_X_pow` `isRoot_comp` `eval_pow` `eval_X` `dvd_iff_isRoot` `zero_add`

Polynomial.Monic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`expand` 📖	mathematical	`Polynomial.Monic` `CommSemiring.toSemiring`	`DFunLike.coe` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.expand`	—	`Polynomial.monic_expand_iff`

---

← Back to Index