Theorems · Theorem · field theory
Polynomial.aroots_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], p.aroots S = (Polynomial.map (algebraMap T S) p).roots- Defined in
- Mathlib.Algebra.Polynomial.Roots
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 131 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- Polynomialstatement and proof · cited by 5,681
- Algebra.algebraMapstatement · cited by 4,706
- Multisetstatement · cited by 2,627
- IsDomainstatement and proof · cited by 2,196
- Polynomial.mapstatement · cited by 806
- Polynomial.rootsstatement · cited by 264
- Polynomial.arootsstatement · cited by 89
Cited by17
Results whose statement or proof uses this declaration.
- Polynomial.aroots_mulproof · cited by 4
- Polynomial.aroots_Cproof · cited by 3
- Polynomial.aroots_C_mulproof · cited by 3
- Polynomial.aroots_Xproof · cited by 2
- Polynomial.aroots_X_sub_Cproof · cited by 2
- Polynomial.aroots_powproof · cited by 2
- integralClosure.mem_lifts_of_monic_of_dvd_mapproof · cited by 1
- Polynomial.natSepDegree_le_natDegreeproof · cited by 1
- Polynomial.aroots_mapproof · cited by 1
- Polynomial.SplittingFieldAux.adjoin_rootSetproof · cited by 0
- Polynomial.eq_mul_mul_of_aroots_quadratic_eq_pairproof · cited by 0
- Polynomial.eq_neg_mul_add_of_aroots_quadratic_eq_pairproof · cited by 0