Theorems · Theorem · field theory
Polynomial.mem_aroots
∀ {S : Type v} {T : Type w} [inst : CommRing T] [IsDomain T] [inst_2 : CommRing S] [inst_3 : IsDomain S]
[inst_4 : Algebra T S] [Module.IsTorsionFree T S] {p : Polynomial T} {a : S},
a ∈ p.aroots S ↔ p ≠ 0 ∧ (Polynomial.aeval a) p = 0- Defined in
- Mathlib.Algebra.Polynomial.Roots
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 134 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- Polynomialstatement and proof · cited by 5,681
- AlgHomstatement · cited by 3,236
- Multisetstatement · cited by 2,627
- IsDomainstatement and proof · cited by 2,196
- Polynomial.aevalstatement and proof · cited by 615
- Module.IsTorsionFreestatement and proof · cited by 600
- FaithfulSMul.algebraMap_injectiveproof · cited by 198
- Polynomial.arootsstatement · cited by 89
- Polynomial.map_ne_zero_iffproof · cited by 12
Cited by8
Results whose statement or proof uses this declaration.
- IsConjRoot.eq_algebraMap_of_injectiveproof · cited by 3
- IntermediateField.algHomAdjoinIntegralEquiv_symm_apply_genproof · cited by 2
- IntermediateField.exists_algHom_adjoin_of_splits_of_aevalproof · cited by 1
- Polynomial.natSepDegree_ne_zeroproof · cited by 1
- isConjRoot_iff_mem_minpoly_arootsproof · cited by 1
- Polynomial.pow_eq_one_of_mahlerMeasure_eq_oneproof · cited by 1
- IntermediateField.Lifts.exists_lift_of_splits'proof · cited by 1
- Polynomial.cyclotomic_dvd_of_mahlerMeasure_eq_oneproof · cited by 0