feat(field_theory/intermediate_field): `minpoly K x = minpoly K (x : …

…L)` (#15946)

This PR adds a lemma stating that `minpoly K x = minpoly K (x : L)` for `x : S` and `S : intermediate_field K L`.

src/field_theory/adjoin.lean

@@ -951,9 +951,9 @@ lemma is_algebraic_supr {ι : Type*} {f : ι → intermediate_field K L}
 begin
   rintros ⟨x, hx⟩,
   obtain ⟨s, hx⟩ := exists_finset_of_mem_supr' hx,
-  rw [algebraic_iff, subtype.coe_mk, ←subtype.coe_mk x hx, ←algebraic_iff],
+  rw [is_algebraic_iff, subtype.coe_mk, ←subtype.coe_mk x hx, ←is_algebraic_iff],
   haveI : ∀ i : (Σ i, f i), finite_dimensional K K⟮(i.2 : L)⟯ :=
-  λ ⟨i, x⟩, adjoin.finite_dimensional (is_algebraic_iff_is_integral.mp (algebraic_iff.mp (h i x))),
+  λ ⟨i, x⟩, adjoin.finite_dimensional (is_integral_iff.1 (is_algebraic_iff_is_integral.1 (h i x))),
   apply algebra.is_algebraic_of_finite,
 end
 

src/field_theory/intermediate_field.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
 
+import field_theory.minpoly
 import field_theory.subfield
 import field_theory.tower
-import ring_theory.algebraic
 
 /-!
 # Intermediate fields
@@ -484,9 +484,19 @@ eq_of_le_of_finrank_le' h_le h_finrank.le
 
 end finite_dimensional
 
-lemma algebraic_iff {x : S} : is_algebraic K x ↔ is_algebraic K (x : L) :=
+lemma is_algebraic_iff {x : S} : is_algebraic K x ↔ is_algebraic K (x : L) :=
 (is_algebraic_algebra_map_iff (algebra_map S L).injective).symm
 
+lemma is_integral_iff {x : S} : is_integral K x ↔ is_integral K (x : L) :=
+by rw [←is_algebraic_iff_is_integral, is_algebraic_iff, is_algebraic_iff_is_integral]
+
+lemma minpoly_eq (x : S) : minpoly K x = minpoly K (x : L) :=
+begin
+  by_cases hx : is_integral K x,
+  { exact minpoly.eq_of_algebra_map_eq (algebra_map S L).injective hx rfl },
+  { exact (minpoly.eq_zero hx).trans (minpoly.eq_zero (mt is_integral_iff.mpr hx)).symm },
+end
+
 end intermediate_field
 
 /-- If `L/K` is algebraic, the `K`-subalgebras of `L` are all fields.  -/