Expand

📁 Source: Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean

Statistics

Metric	Count
Definitions	0
Theorems cyclotomic_expand_eq_cyclotomic, cyclotomic_expand_eq_cyclotomic_mul, cyclotomic_irreducible_of_irreducible_pow, cyclotomic_irreducible_pow_of_irreducible_pow, cyclotomic_mul_prime_dvd_eq_pow, cyclotomic_mul_prime_eq_pow_of_not_dvd, cyclotomic_mul_prime_pow_eq, cyclotomic_six, isRoot_cyclotomic_prime_pow_mul_iff_of_charP	9
Total	9

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cyclotomic_expand_eq_cyclotomic 📖	mathematical	Nat.Prime	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike expand cyclotomic CommRing.toRing	—	cyclotomic_zero map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass MulZeroClass.zero_mul eq_of_monic_of_dvd_of_natDegree_le cyclotomic.monic Monic.expand Nat.Prime.pos Nat.instAtLeastTwoHAddOfNat Complex.isPrimitiveRoot_exp LT.lt.ne cyclotomic_eq_minpoly Complex.instCharZero minpoly.isIntegrallyClosed_dvd Int.instIsDomain IsDedekindRing.toIsIntegralClosure IsDedekindDomain.toIsDedekindRing IsPrincipalIdealRing.isDedekindDomain EuclideanDomain.to_principal_ideal_domain instIsDomain instIsTorsionFreeIntOfIsAddTorsionFree Complex.instIsAddTorsionFree IsPrimitiveRoot.isIntegral eval_map_algebraMap map_expand map_cyclotomic expand_eval IsRoot.def isRoot_cyclotomic_iff NeZero.charZero NeZero.of_pos IsPrimitiveRoot.pow_of_dvd Nat.Prime.ne_zero dvd_mul_left natDegree_expand natDegree_cyclotomic Int.instNontrivial mul_comm Nat.totient_mul_of_prime_of_dvd le_refl map_cyclotomic_int
cyclotomic_expand_eq_cyclotomic_mul 📖	mathematical	Nat.Prime	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike expand cyclotomic CommRing.toRing Ring.toSemiring instMul	—	cyclotomic_zero map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass MulZeroClass.zero_mul mul_one eq_of_monic_of_dvd_of_natDegree_le Monic.mul cyclotomic.monic Monic.expand Nat.Prime.pos IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast IsPrimitive.mul cyclotomic.isPrimitive Monic.isPrimitive map_mul map_cyclotomic_int map_expand IsCoprime.mul_dvd cyclotomic.isCoprime_rat Nat.Prime.ne_one mul_left_cancel₀ IsCancelMulZero.toIsLeftCancelMulZero Nat.instIsCancelMulZero LT.lt.ne' mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.instAtLeastTwoHAddOfNat Complex.isPrimitiveRoot_exp Complex.instCharZero cyclotomic_eq_minpoly_rat minpoly.dvd eval_map_algebraMap map_cyclotomic expand_eval IsRoot.def isRoot_cyclotomic_iff instIsDomain NeZero.charZero NeZero.of_pos IsPrimitiveRoot.pow_of_dvd Nat.Prime.ne_zero dvd_mul_left LT.lt.ne IsPrimitiveRoot.pow_of_prime natDegree_expand natDegree_cyclotomic Int.instNontrivial natDegree_mul NormMulClass.toNoZeroDivisors Int.instNormMulClass cyclotomic_ne_zero mul_comm Nat.totient_mul Nat.Prime.coprime_iff_not_dvd Nat.totient_prime le_refl
cyclotomic_irreducible_of_irreducible_pow 📖	—	Nat.Prime Irreducible Polynomial Ring.toSemiring CommRing.toRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring cyclotomic Monoid.toNatPow Nat.instMonoid	—	—	cyclotomic_irreducible_pow_of_irreducible_pow Ne.bot_lt pow_one
cyclotomic_irreducible_pow_of_irreducible_pow 📖	—	Nat.Prime Irreducible Polynomial Ring.toSemiring CommRing.toRing MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring cyclotomic Monoid.toNatPow Nat.instMonoid	—	—	pow_zero cyclotomic_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass irreducible_X_sub_C add_zero LT.lt.ne' add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid of_irreducible_expand Nat.Prime.ne_zero cyclotomic_expand_eq_cyclotomic dvd_pow_self pow_succ
cyclotomic_mul_prime_dvd_eq_pow 📖	mathematical	—	cyclotomic Polynomial Ring.toSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	ZMod.expand_card map_cyclotomic_int map_expand cyclotomic_expand_eq_cyclotomic Fact.out map_cyclotomic map_pow
cyclotomic_mul_prime_eq_pow_of_not_dvd 📖	mathematical	—	cyclotomic Polynomial Ring.toSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	mul_right_injective₀ instIsLeftCancelMulZeroOfIsCancelAdd AddCancelMonoid.toIsCancelAdd IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero ZMod.instIsDomain cyclotomic_ne_zero ZMod.nontrivial Nat.Prime.one_lt' pow_succ' tsub_add_cancel_of_le StarOrderedRing.toExistsAddOfLE Nat.instStarOrderedRing IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub LT.lt.le Nat.Prime.one_lt Fact.out mul_comm ZMod.expand_card map_cyclotomic_int map_expand cyclotomic_expand_eq_cyclotomic_mul map_mul map_cyclotomic map_pow
cyclotomic_mul_prime_pow_eq 📖	mathematical	—	cyclotomic Monoid.toNatPow Nat.instMonoid Polynomial Ring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	pow_one pow_zero mul_comm cyclotomic_mul_prime_eq_pow_of_not_dvd mul_assoc pow_succ' cyclotomic_mul_prime_dvd_eq_pow pow_mul tsub_zero Nat.instOrderedSub pow_succ
cyclotomic_six 📖	mathematical	—	cyclotomic Polynomial Ring.toSemiring instAdd instSub Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring X instOne	—	mul_right_cancel₀ instIsRightCancelMulZeroOfIsCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsCancelMulZero.toIsRightCancelMulZero Int.instIsCancelMulZero cyclotomic_ne_zero Int.instNontrivial cyclotomic_expand_eq_cyclotomic_mul Nat.prime_three Mathlib.Meta.NormNum.isNat_dvd_false Mathlib.Meta.NormNum.isNat_ofNat cyclotomic_two map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass expand_X map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add map_cyclotomic_int map_add map_sub map_pow map_X map_one
isRoot_cyclotomic_prime_pow_mul_iff_of_charP 📖	mathematical	—	IsRoot Ring.toSemiring CommRing.toRing cyclotomic Monoid.toNatPow Nat.instMonoid IsPrimitiveRoot CommRing.toCommMonoid	—	pow_zero one_mul isRoot_cyclotomic_iff eq_zero_of_pow_eq_zero isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors eval_pow cyclotomic_mul_prime_pow_eq NeZero.not_char_dvd IsRoot.def zero_pow pow_right_strictMono₀ LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.instZeroLEOneClass Nat.Prime.one_lt Fact.out LT.lt.ne'

---

← Back to Index