Theorems · Theorem · field theory
Polynomial.mem_rootSet_of_ne
∀ {T : Type w} [inst : CommRing T] {p : Polynomial T} {S : Type u_1} [IsDomain T] [inst_2 : CommRing S]
[inst_3 : IsDomain S] [inst_4 : Algebra T S] [Module.IsTorsionFree T S],
p ≠ 0 → ∀ {a : S}, a ∈ p.rootSet S ↔ (Polynomial.aeval a) p = 0- Defined in
- Mathlib.Algebra.Polynomial.Roots
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 136 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Setstatement · cited by 53,352
- 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
- IsDomainstatement and proof · cited by 2,196
- Polynomial.aevalstatement · cited by 615
- Module.IsTorsionFreestatement and proof · cited by 600
- Polynomial.rootSetstatement · cited by 101
- Polynomial.mem_rootSetproof · cited by 13
Cited by10
Results whose statement or proof uses this declaration.
- Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splitsproof · cited by 2
- GaloisField.finrankproof · cited by 2
- Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_invproof · cited by 2
- gal_X_pow_sub_C_isSolvable_auxproof · cited by 1
- gal_X_pow_sub_one_isSolvableproof · cited by 1
- Polynomial.preimage_eval_singletonproof · cited by 1
- isSplittingField_X_pow_sub_C_of_root_adjoin_eq_topproof · cited by 1
- Algebra.IsAlgebraic.normalClosure_le_iSup_adjoinproof · cited by 1
- IntermediateField.exists_finset_of_mem_supr''proof · cited by 0
- isSplittingField_AdjoinRoot_X_pow_sub_Cproof · cited by 0