Theorems · Theorem · field theory
Polynomial.rootSet_def
∀ {T : Type w} [inst : CommRing T] (p : Polynomial T) (S : Type u_1) [inst_1 : CommRing S] [inst_2 : IsDomain S]
[inst_3 : Algebra T S] [inst_4 : DecidableEq S], p.rootSet S = ↑(p.aroots S).toFinset- Defined in
- Mathlib.Algebra.Polynomial.Roots
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 133 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.
- Setstatement and proof · cited by 53,352
- CommRingstatement and proof · cited by 17,173
- Finsetstatement and proof · cited by 13,712
- Algebrastatement and proof · cited by 11,388
- SetLike.coestatement and proof · cited by 8,199
- Polynomialstatement and proof · cited by 5,681
- Multisetproof · cited by 2,627
- IsDomainstatement and proof · cited by 2,196
- SetLikeproof · cited by 1,084
- Multiset.toFinsetstatement and proof · cited by 230
- Classical.decEqproof · cited by 134
- Polynomial.rootSetstatement · cited by 101
Cited by12
Results whose statement or proof uses this declaration.
- Polynomial.mem_rootSet'proof · cited by 8
- IntermediateField.splits_of_splitsproof · cited by 5
- Polynomial.card_rootSet_eq_natDegreeproof · cited by 3
- Polynomial.rootSet_Cproof · cited by 3
- Polynomial.natSepDegree_eq_natDegree_iffproof · cited by 2
- ConjRootClass.aroots_minpoly_eq_carrier_valproof · cited by 1
- Polynomial.Gal.galActionHom_bijective_of_prime_degreeproof · cited by 1
- Polynomial.card_rootSet_eq_natDegree_iff_of_splitsproof · cited by 1
- Polynomial.Gal.restrictProd_injectiveproof · cited by 1
- Polynomial.SplittingFieldAux.adjoin_rootSetproof · cited by 0
- Polynomial.card_rootSet_le_derivativeproof · cited by 0
- ConjRootClass.minpoly.map_eq_prodproof · cited by 0