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.toPow 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.toPow 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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	eval₂_X
expand_aeval 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval expand Monoid.toPow 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.toPow 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	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring semiring 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	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring semiring 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.toPow 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.toPow 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.toPow 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.toPow 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.toPow 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.toPow 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.toPow 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 📖	mathematical	Irreducible Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring DFunLike.coe AlgHom algebraOfAlgebra Algebra.id AlgHom.funLike expand	Irreducible Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	isLocalHom_expand Ne.bot_lt Irreducible.of_map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
of_irreducible_expand_pow 📖	mathematical	Irreducible Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring DFunLike.coe AlgHom algebraOfAlgebra Algebra.id AlgHom.funLike expand Monoid.toPow Nat.instMonoid	Irreducible Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	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.toPow 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.toPow 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	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