Documentation

Mathlib.FieldTheory.Minpoly.Basic

Minimal polynomials #

This file defines the minimal polynomial of an element x of an A-algebra B, under the assumption that x is integral over A, and derives some basic properties such as irreducibility under the assumption B is a domain.

noncomputable def minpoly (A : Type u_1) {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] (x : B) :

Suppose x : B, where B is an A-algebra.

The minimal polynomial minpoly A x of x is a monic polynomial with coefficients in A of smallest degree that has x as its root, if such exists (IsIntegral A x) or zero otherwise.

For example, if V is a 𝕜-vector space for some field 𝕜 and f : V →ₗ[𝕜] V then the minimal polynomial of f is minpoly 𝕜 f.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem minpoly.monic {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] {x : B} (hx : IsIntegral A x) :

    A minimal polynomial is monic.

    theorem minpoly.ne_zero {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] {x : B} [Nontrivial A] (hx : IsIntegral A x) :
    minpoly A x 0

    A minimal polynomial is nonzero.

    theorem minpoly.eq_zero {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] {x : B} (hx : ¬IsIntegral A x) :
    minpoly A x = 0
    theorem minpoly.algHom_eq {A : Type u_1} {B : Type u_2} {B' : Type u_3} [CommRing A] [Ring B] [Ring B'] [Algebra A B] [Algebra A B'] (f : B →ₐ[A] B') (hf : Function.Injective f) (x : B) :
    minpoly A (f x) = minpoly A x
    theorem minpoly.algebraMap_eq {A : Type u_1} {B' : Type u_3} [CommRing A] [Ring B'] [Algebra A B'] {B : Type u_4} [CommRing B] [Algebra A B] [Algebra B B'] [IsScalarTower A B B'] (h : Function.Injective (algebraMap B B')) (x : B) :
    minpoly A ((algebraMap B B') x) = minpoly A x
    @[simp]
    theorem minpoly.algEquiv_eq {A : Type u_1} {B : Type u_2} {B' : Type u_3} [CommRing A] [Ring B] [Ring B'] [Algebra A B] [Algebra A B'] (f : B ≃ₐ[A] B') (x : B) :
    minpoly A (f x) = minpoly A x
    @[simp]
    theorem minpoly.aeval (A : Type u_1) {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] (x : B) :

    An element is a root of its minimal polynomial.

    theorem minpoly.ne_one (A : Type u_1) {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] (x : B) [Nontrivial B] :
    minpoly A x 1

    A minimal polynomial is not 1.

    theorem minpoly.map_ne_one (A : Type u_1) {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] (x : B) [Nontrivial B] {R : Type u_4} [Semiring R] [Nontrivial R] (f : A →+* R) :
    theorem minpoly.not_isUnit (A : Type u_1) {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] (x : B) [Nontrivial B] :

    A minimal polynomial is not a unit.

    theorem minpoly.mem_range_of_degree_eq_one (A : Type u_1) {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] (x : B) (hx : Polynomial.degree (minpoly A x) = 1) :
    theorem minpoly.min (A : Type u_1) {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] (x : B) {p : Polynomial A} (pmonic : Polynomial.Monic p) (hp : (Polynomial.aeval x) p = 0) :

    The defining property of the minimal polynomial of an element x: it is the monic polynomial with smallest degree that has x as its root.

    theorem minpoly.unique' (A : Type u_1) {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] (x : B) {p : Polynomial A} (hm : Polynomial.Monic p) (hp : (Polynomial.aeval x) p = 0) (hl : ∀ (q : Polynomial A), Polynomial.degree q < Polynomial.degree pq = 0 (Polynomial.aeval x) q 0) :
    p = minpoly A x
    theorem minpoly.subsingleton (A : Type u_1) {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] (x : B) [Subsingleton B] :
    minpoly A x = 1
    theorem minpoly.natDegree_pos {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] {x : B} [Nontrivial B] (hx : IsIntegral A x) :

    The degree of a minimal polynomial, as a natural number, is positive.

    theorem minpoly.degree_pos {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] {x : B} [Nontrivial B] (hx : IsIntegral A x) :

    The degree of a minimal polynomial is positive.

    theorem minpoly.degree_eq_one_iff {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] {x : B} [Nontrivial B] :
    theorem minpoly.two_le_natDegree_iff {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] {x : B} [Nontrivial B] (int : IsIntegral A x) :
    theorem minpoly.two_le_natDegree_subalgebra {A : Type u_1} [CommRing A] {B : Type u_4} [CommRing B] [Algebra A B] [Nontrivial B] {S : Subalgebra A B} {x : B} (int : IsIntegral (S) x) :
    2 Polynomial.natDegree (minpoly (S) x) xS
    theorem minpoly.eq_X_sub_C_of_algebraMap_inj {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] (a : A) (hf : Function.Injective (algebraMap A B)) :
    minpoly A ((algebraMap A B) a) = Polynomial.X - Polynomial.C a

    If B/A is an injective ring extension, and a is an element of A, then the minimal polynomial of algebraMap A B a is X - C a.

    theorem minpoly.aeval_ne_zero_of_dvdNotUnit_minpoly {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] {x : B} {a : Polynomial A} (hx : IsIntegral A x) (hamonic : Polynomial.Monic a) (hdvd : DvdNotUnit a (minpoly A x)) :

    If a strictly divides the minimal polynomial of x, then x cannot be a root for a.

    theorem minpoly.irreducible {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] {x : B} [IsDomain A] [IsDomain B] (hx : IsIntegral A x) :

    A minimal polynomial is irreducible.