Theorems · Definition · field theory
minpolyDiv
(R : Type u_1) → {S : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → S → Polynomial SminpolyDiv R x : S[X] for x : S is the polynomial minpoly R x / (X - C x).
- Defined in
- Mathlib.FieldTheory.Minpoly.MinpolyDiv
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- Polynomialstatement · cited by 5,681
- Algebra.algebraMapproof · cited by 4,706
- Polynomial.Xproof · cited by 1,639
- Polynomial.Cproof · cited by 1,598
- Polynomial.mapproof · cited by 806
- minpolyproof · cited by 439
- Polynomial.divByMonicproof · cited by 77
Cited by20
Results whose statement or proof uses this declaration.
- minpolyDiv_specstatement · cited by 7
- natDegree_minpolyDiv_succstatement and proof · cited by 4
- minpolyDiv_ne_zerostatement and proof · cited by 2
- eval₂_minpolyDiv_of_eval₂_eq_zerostatement and proof · cited by 2
- coeff_minpolyDivstatement and proof · cited by 2
- natDegree_minpolyDiv_ltstatement and proof · cited by 1
- minpolyDiv_eq_of_isIntegrallyClosedstatement · cited by 1
- minpolyDiv_eq_zerostatement · cited by 1
- minpolyDiv_monicstatement and proof · cited by 1
- sum_smul_minpolyDiv_eq_X_powstatement and proof · cited by 1
- eval_minpolyDiv_selfstatement and proof · cited by 1
- eval₂_minpolyDiv_selfstatement · cited by 1