Theorems · Theorem · field theory
minpolyDiv_spec
∀ (R : Type u_2) {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (x : S),
minpolyDiv R x * (Polynomial.X - Polynomial.C x) = Polynomial.map (algebraMap R S) (minpoly R x)- Defined in
- Mathlib.FieldTheory.Minpoly.MinpolyDiv
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
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
- RingHomstatement · cited by 10,189
- Polynomialstatement and proof · cited by 5,681
- Algebra.algebraMapstatement and proof · cited by 4,706
- mul_commproof · cited by 2,262
- Polynomial.Xstatement and proof · cited by 1,639
- Polynomial.Cstatement and proof · cited by 1,598
- Polynomial.mapstatement and proof · cited by 806
- minpolystatement and proof · cited by 439
- minpoly.aevalproof · cited by 91
Cited by7
Results whose statement or proof uses this declaration.
- natDegree_minpolyDiv_succproof · cited by 4
- coeff_minpolyDivproof · cited by 2
- minpolyDiv_ne_zeroproof · cited by 2
- eval₂_minpolyDiv_of_eval₂_eq_zeroproof · cited by 2
- minpolyDiv_monicproof · cited by 1
- eval_minpolyDiv_selfproof · cited by 1
- minpolyDiv_eval_eq_zero_of_ne_of_aeval_eq_zeroproof · cited by 0