[Merged by Bors] - feat(field_theory/normal): Splitting field is normal

[tb65536]

Proves that splitting fields are normal.

---

• depends on: [Merged by Bors] - refactor(ring_theory): change field instance on adjoin_root #5759
• depends on: [Merged by Bors] - feat(field_theory/adjoin): Inductively construct algebra homomorphism #5765
• depends on: feat(field_theory/intermediate_field): to_subalgebra_le_iff #5766
• depends on: [Merged by Bors] - feat(ring_theory/algebra_tower): Restriction of adjoin #5767

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - refactor(ring_theory): change field instance on adjoin_root #5759
• [Merged by Bors] - feat(field_theory/adjoin): Inductively construct algebra homomorphism #5765
• feat(field_theory/intermediate_field): to_subalgebra_le_iff #5766
• [Merged by Bors] - feat(ring_theory/algebra_tower): Restriction of adjoin #5767

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[jcommelin]

Nice! The proof is longish, and seems to spend quite some time on setting up the right type class instances (unfortunately). I'm not sure if we can do much about that. But I'm wondering... do you think there are parts that could be made reusable by putting them in separate lemmas?
(I haven't opened the PR in VScode yet.)

[tb65536]

It's hard to extract lemmas since a lot of the proof depends on the specific setup. One possibility that I see is this lemma which would shorten the proof of suffices : nonempty (D →ₐ[F] E),

lemma lem1 {F E K : Type*} [field F] [field E] [field K] [algebra F E] [algebra E K] [algebra F K]
  [finite_dimensional F E] [finite_dimensional F K]
  [is_scalar_tower F E K] (ϕ : K →ₐ[F] E) : finite_dimensional.findim E K = 1 :=
begin
  have nat_lemma : ∀ a b c : ℕ, a * b = c → c ≤ a → 0 < c → b = 1,
  { intros a b c h1 h2 h3, nlinarith },
  exact nat_lemma _ _ _ (finite_dimensional.findim_mul_findim F E K)
    (linear_map.findim_le_findim_of_injective (show function.injective ϕ.to_linear_map,
      from ϕ.to_ring_hom.injective)) finite_dimensional.findim_pos,
end

(I guess you can weaken the hypotheses to the same as for findim_mul_findim)

[jcommelin]

Thanks 🎉

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Build failed:

• Build mathlib

[jcommelin]

Sorry, this file needs to be updated to the new minpoly syntax.

bors r-

bors d+

[bors]

✌️ tb65536 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[tb65536]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests