Minimal polynomials on a finite algebra

This file proves the bound on the degree of a minimal polynomial on an algebra that is finite as a module.

theorem minpoly.natDegree_le_spanFinrank (A : Type u_1) {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] [Module.Finite A B] (x : B) : (minpoly A x).natDegree ≤ ⊤.spanFinrank

theorem minpoly.natDegree_le {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] [Module.Finite A B] (x : B) [Module.Free A B] : (minpoly A x).natDegree ≤ Module.finrank A B

theorem minpoly.degree_le {A : Type u_1} {B : Type u_2} [CommRing A] [Ring B] [Algebra A B] [Module.Finite A B] (x : B) [Module.Free A B] : (minpoly A x).degree ≤ ↑(Module.finrank A B)