feat(field_theory/normal): normal_of_alg_equiv (#5225)

Proves that normal is preserved by an alg_equiv

src/field_theory/normal.lean

@@ -68,4 +68,25 @@ begin
     (minimal_polynomial.dvd_map_of_is_scalar_tower K hx)⟩,
 end
 
+variables {F} {E} {E' : Type*} [field E'] [algebra F E']
+
+lemma normal.of_alg_equiv [h : normal F E] (f : E ≃ₐ[F] E') : normal F E' :=
+begin
+  intro x,
+  cases h (f.symm x) with hx hhx,
+  have H := is_integral_alg_hom f.to_alg_hom hx,
+  rw [alg_equiv.to_alg_hom_eq_coe, alg_equiv.coe_alg_hom, alg_equiv.apply_symm_apply] at H,
+  use H,
+  apply polynomial.splits_of_splits_of_dvd (algebra_map F E') (minimal_polynomial.ne_zero hx),
+  { rw ← alg_hom.comp_algebra_map f.to_alg_hom,
+    exact polynomial.splits_comp_of_splits (algebra_map F E) f.to_alg_hom.to_ring_hom hhx },
+  { apply minimal_polynomial.dvd H,
+    rw ← add_equiv.map_eq_zero_iff f.symm.to_add_equiv,
+    exact eq.trans (polynomial.aeval_alg_hom_apply f.symm.to_alg_hom x
+      (minimal_polynomial hx)).symm (minimal_polynomial.aeval hx) },
+end
+
+lemma alg_equiv.transfer_normal (f : E ≃ₐ[F] E') : normal F E ↔ normal F E' :=
+⟨λ h, by exactI normal.of_alg_equiv f, λ h, by exactI normal.of_alg_equiv f.symm⟩
+
 end normal_tower