Basic

📁 Source: Mathlib/Analysis/Complex/Polynomial/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_root, isAlgClosed, degree_le_two, natDegree_le_two, card_complex_roots_eq_card_real_add_card_not_gal_inv, galActionHom_bijective_of_prime_degree, galActionHom_bijective_of_prime_degree', splits_ℚ_ℂ, mul_star_dvd_of_aeval_eq_zero_im_ne_zero, quadratic_dvd_of_aeval_eq_zero_im_ne_zero, nonempty_algEquiv_or	11
Total	11

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_root 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass Polynomial.degree Complex instSemiring	Polynomial.IsRoot	—	Differentiable.apply_eq_of_tendsto_cocompact instNontrivial Differentiable.inv Polynomial.differentiable Filter.Tendsto.comp Filter.tendsto_inv₀_cobounded Polynomial.tendsto_norm_atTop isAbsoluteValueNorm tendsto_norm_cobounded_atTop Metric.cobounded_eq_cocompact instProperSpace map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Polynomial.funext instIsDomain CharZero.infinite instCharZero inv_injective Polynomial.eval_zero inv_zero
isAlgClosed 📖	mathematical	—	IsAlgClosed Complex instField	—	IsAlgClosed.of_exists_root exists_root Polynomial.degree_pos_of_irreducible

Irreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
degree_le_two 📖	mathematical	Irreducible Polynomial Real Real.semiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder Polynomial.degree instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	Polynomial.natDegree_le_iff_degree_le natDegree_le_two
natDegree_le_two 📖	mathematical	Irreducible Polynomial Real Real.semiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	Polynomial.natDegree	—	IsAlgClosed.exists_aeval_eq_zero Complex.isAlgClosed instFaithfulSMul_1 DivisionRing.isSimpleRing Complex.instNontrivial LT.lt.ne' Polynomial.degree_pos_of_irreducible Complex.finrank_real_complex minpoly.eq_of_irreducible Polynomial.natDegree_mul NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass ne_zero Polynomial.nontrivial Real.instNontrivial RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Polynomial.natDegree_C add_zero minpoly.natDegree_le Complex.instFiniteDimensionalReal

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_star_dvd_of_aeval_eq_zero_im_ne_zero 📖	mathematical	DFunLike.coe AlgHom Real Polynomial CommSemiring.toSemiring Real.instCommSemiring Complex semiring Complex.instSemiring algebraOfAlgebra Algebra.id NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField RCLike.toNormedAlgebra Complex.instRCLike AlgHom.funLike aeval Complex.instZero	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing Complex.commRing instMul instSub Complex.instRing X RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C Complex.instCommSemiring starRingEnd Complex.instStarRing map algebraMap	—	IsCoprime.mul_dvd isCoprime_X_sub_C_of_isUnit_sub sub_ne_zero Complex.conj_eq_iff_im eval_map_algebraMap aeval_conj Complex.instNontrivial RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
quadratic_dvd_of_aeval_eq_zero_im_ne_zero 📖	mathematical	DFunLike.coe AlgHom Real Polynomial CommSemiring.toSemiring Real.instCommSemiring Complex semiring Complex.instSemiring algebraOfAlgebra Algebra.id NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField RCLike.toNormedAlgebra Complex.instRCLike AlgHom.funLike aeval Complex.instZero	Real.semiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing Real.commRing instAdd instSub Real.instRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X instMul RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.re Real.instMonoid Norm.norm Complex.instNorm	—	Nat.instAtLeastTwoHAddOfNat map_dvd_map' map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_add map_sub map_pow map_X map_mul map_C Complex.ofReal_mul Complex.add_conj map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass Complex.mul_conj' Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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 Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pf_right 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.add_pf_add_gt Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsInt.to_isNat mul_star_dvd_of_aeval_eq_zero_im_ne_zero

Polynomial.Gal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_complex_roots_eq_card_real_add_card_not_gal_inv 📖	mathematical	—	Finset.card Complex Set.toFinset Polynomial.rootSet Rat.commRing Complex.commRing instIsDomain Field.toSemifield Complex.instField DivisionRing.toRatAlgebra NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Complex.instNormedField Complex.instCharZero Polynomial.rootSetFintype Real Real.commRing Real.instIsDomain Real.instDivisionRing RCLike.charZero_rclike Real.instRCLike Set.Elem EuclideanDomain.toCommRing Field.toEuclideanDomain Rat.instField Equiv.Perm.support Set Set.instMembership Complex.instDecidableEq DFunLike.coe MonoidHom Polynomial.Gal Equiv.Perm MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Polynomial.instGroupGal Equiv.Perm.permGroup MonoidHom.instFunLike galActionHom splits_ℚ_ℂ AlgEquiv Semifield.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgEquiv.aut restrict AlgEquiv.restrictScalars Rat.commSemiring Real.instCommSemiring Algebra.complexToReal Complex.instSemiring Algebra.id Complex.instCommSemiring IsScalarTower.rat SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Complex.addCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedCommRing InnerProductSpace.toNormedSpace instInnerProductSpaceRealComplex Rat.instNormedField NormedAlgebra.toNormedSpace normedAlgebraRat RCLike.toNormedAlgebra Complex.instRCLike Complex.conjAe	—	instIsDomain Complex.instCharZero Real.instIsDomain RCLike.charZero_rclike splits_ℚ_ℂ IsScalarTower.rat Finset.eq_empty_of_isEmpty Polynomial.rootSet_zero Set.instIsEmptyElemEmptyCollection Set.toFinset_congr Set.toFinset_empty RingHom.injective DivisionRing.isSimpleRing Complex.instNontrivial Finset.card_image_of_injective Subtype.coe_injective Set.mem_toFinset Polynomial.mem_rootSet_of_ne Rat.isDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Polynomial.aeval_algHom_apply AlgHom.algHomClass map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass Complex.ext galActionHom_restrict Complex.conj_eq_iff_im Polynomial.mem_rootSet Equiv.Perm.mem_support Finset.card_union_of_disjoint Finset.disjoint_left
galActionHom_bijective_of_prime_degree 📖	mathematical	Irreducible Polynomial Rat.semiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Nat.Prime Polynomial.natDegree Fintype.card Set.Elem Complex Polynomial.rootSet Rat.commRing Complex.commRing instIsDomain Field.toSemifield Complex.instField DivisionRing.toRatAlgebra NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Complex.instNormedField Complex.instCharZero Polynomial.rootSetFintype Real Real.commRing Real.instIsDomain Real.instDivisionRing RCLike.charZero_rclike Real.instRCLike	Function.Bijective Polynomial.Gal Rat.instField Equiv.Perm EuclideanDomain.toCommRing Field.toEuclideanDomain DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Polynomial.instGroupGal Equiv.Perm.permGroup MonoidHom.instFunLike galActionHom splits_ℚ_ℂ	—	instIsDomain Complex.instCharZero Real.instIsDomain RCLike.charZero_rclike Fintype.card_congr' Polynomial.rootSet_def Fintype.card_coe Multiset.toFinset_card_of_nodup Polynomial.nodup_roots Polynomial.separable_map Complex.instNontrivial Irreducible.separable Rat.instCharZero Polynomial.Splits.natDegree_eq_card_roots IsAlgClosed.splits Complex.isAlgClosed Polynomial.natDegree_map DivisionRing.isSimpleRing splits_ℚ_ℂ IsScalarTower.rat galActionHom_injective Equiv.Perm.subgroup_eq_top_of_swap_mem Fintype.card_eq_nat_card Nat.card_congr prime_degree_dvd_card Equiv.Perm.card_support_eq_two Set.toFinset_card card_complex_roots_eq_card_real_add_card_not_gal_inv Subgroup.mem_top
galActionHom_bijective_of_prime_degree' 📖	mathematical	Irreducible Polynomial Rat.semiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Nat.Prime Polynomial.natDegree Fintype.card Set.Elem Real Polynomial.rootSet Rat.commRing Real.commRing Real.instIsDomain DivisionRing.toRatAlgebra Real.instDivisionRing RCLike.charZero_rclike Real.instRCLike Polynomial.rootSetFintype Complex Complex.commRing instIsDomain Field.toSemifield Complex.instField NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Complex.instNormedField Complex.instCharZero	Function.Bijective Polynomial.Gal Rat.instField Equiv.Perm EuclideanDomain.toCommRing Field.toEuclideanDomain DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Polynomial.instGroupGal Equiv.Perm.permGroup MonoidHom.instFunLike galActionHom splits_ℚ_ℂ	—	Real.instIsDomain RCLike.charZero_rclike instIsDomain Complex.instCharZero galActionHom_bijective_of_prime_degree splits_ℚ_ℂ IsScalarTower.rat Equiv.Perm.two_dvd_card_support map_pow MonoidHom.instMonoidHomClass AlgEquiv.ext Complex.conj_conj map_one MonoidHomClass.toOneHomClass card_complex_roots_eq_card_real_add_card_not_gal_inv Set.toFinset_card
splits_ℚ_ℂ 📖	mathematical	—	Fact Polynomial.Splits Complex Complex.instSemiring Polynomial.map CommSemiring.toSemiring Rat.commSemiring algebraMap DivisionRing.toRatAlgebra NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Complex.instNormedField Complex.instCharZero	—	Complex.instCharZero IsAlgClosed.splits Complex.isAlgClosed

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonempty_algEquiv_or 📖	mathematical	—	AlgEquiv Real instCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semiring Algebra.id Complex Complex.instSemiring NormedAlgebra.toAlgebra normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField RCLike.toNormedAlgebra Complex.instRCLike	—	IsAlgClosed.nonempty_algEquiv_or_of_finrank_eq_two Complex.isAlgClosed Complex.finrank_real_complex

---

← Back to Index