Theorems · Theorem · field theory
minpoly.monic
∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B},
IsIntegral A x → (minpoly A x).MonicA minimal polynomial is monic.
- Defined in
- Mathlib.FieldTheory.Minpoly.Basic
- Cited by
- 81 results in Mathlib
- Foundations
- Depth 84 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.
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- Ringstatement and proof · cited by 7,463
- Polynomialproof · cited by 5,681
- Algebra.algebraMapproof · cited by 4,706
- Polynomial.Monicstatement and proof · cited by 461
- minpolystatement · cited by 439
- IsIntegralstatement and proof · cited by 427
- Polynomial.eval₂proof · cited by 267
- WellFounded.min_memproof · cited by 23
- Polynomial.degree_lt_wfproof · cited by 7
Cited by81
Results whose statement or proof uses this declaration.
- minpoly.ne_zeroproof · cited by 44
- minpoly.dvdproof · cited by 31
- minpoly.irreducibleproof · cited by 26
- minpoly.eq_of_irreducible_of_monicproof · cited by 9
- minpoly.isIntegrallyClosed_dvdproof · cited by 9
- minpoly.natDegree_posproof · cited by 8
- Algebra.isIntegral_traceproof · cited by 7
- Polynomial.cyclotomic_eq_minpolyproof · cited by 7
- minpoly.uniqueproof · cited by 7
- IsAlgClosed.algebraMap_bijective_of_isIntegralproof · cited by 6
- minpoly.isIntegrallyClosed_eq_field_fractionsproof · cited by 6
- IsIntegral.coeffproof · cited by 4