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
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) :
    (minpoly A x).Monic

    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) :

    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.ne_zero_iff {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] {x : B} [Nontrivial A] :
    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.

    @[simp]
    theorem minpoly.aeval_algHom (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) :
    (Polynomial.aeval (f x)) (minpoly A x) = 0

    Given any f : B →ₐ[A] B' and any x : L, the minimal polynomial of x vanishes at f x.

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

    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 : (minpoly A x).degree = 1) :
    x ∈ (algebraMap A B).range
    theorem minpoly.min (A : Type u_1) {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] (x : B) {p : Polynomial A} (pmonic : p.Monic) (hp : (Polynomial.aeval x) p = 0) :
    (minpoly A x).degree ≀ p.degree

    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 : p.Monic) (hp : (Polynomial.aeval x) p = 0) (hl : βˆ€ (q : Polynomial A), q.degree < p.degree β†’ q = 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) :
    0 < (minpoly A x).natDegree

    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) :
    0 < (minpoly A x).degree

    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] :
    (minpoly A x).degree = 1 ↔ x ∈ (algebraMap A B).range
    theorem minpoly.natDegree_eq_one_iff {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] {x : B} [Nontrivial B] :
    (minpoly A x).natDegree = 1 ↔ x ∈ (algebraMap A B).range
    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) :
    2 ≀ (minpoly A x).natDegree ↔ x βˆ‰ (algebraMap A B).range
    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 ≀ (minpoly (β†₯S) x).natDegree ↔ x βˆ‰ S
    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 : a.Monic) (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.