Theorems · Theorem · field theory
minpoly.aeval
∀ (A : Type u_1) {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] (x : B),
(Polynomial.aeval x) (minpoly A x) = 0An element is a root of its minimal polynomial.
- Defined in
- Mathlib.FieldTheory.Minpoly.Basic
- Cited by
- 91 results in Mathlib
- Foundations
- Depth 111 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
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
- Ringstatement and proof · cited by 7,463
- Polynomialstatement and proof · cited by 5,681
- Algebra.algebraMapproof · cited by 4,706
- AlgHomstatement · cited by 3,236
- Polynomial.aevalstatement and proof · cited by 615
- Polynomial.Monicproof · cited by 461
- minpolystatement · cited by 439
- IsIntegralproof · cited by 427
- Polynomial.eval₂proof · cited by 267
Cited by91
Results whose statement or proof uses this declaration.
- minpoly.dvdproof · cited by 31
- minpoly.irreducibleproof · cited by 26
- isPurelyInseparable_iff_pow_memproof · cited by 10
- minpoly.dvd_map_of_isScalarTowerproof · cited by 8
- minpoly.natDegree_posproof · cited by 8
- minpolyDiv_specproof · cited by 7
- minpoly.uniqueproof · cited by 7
- IsAlgClosed.algebraMap_bijective_of_isIntegralproof · cited by 6
- minpoly.isIntegrallyClosed_eq_field_fractionsproof · cited by 6
- Algebra.FormallyUnramified.of_isSeparableproof · cited by 5
- IsIntegral.coeffproof · cited by 4
- Algebra.isIntegral_normproof · cited by 4