[Merged by Bors] - feat: Add Polynomial.separable_map'.

[erdOne]

---

[riccardobrasca]

This is strictly more general than the actual separable_map, right? In this case this should be the umprimed version (maybe you can even inline the proof of the weak case and only keep the more general one).

[riccardobrasca]

This is strictly more general than the actual separable_map, right? In this case this should be the umprimed version (maybe you can even inline the proof of the weak case and only keep the more general one).

I mean something like

attribute [local instance] Ideal.Quotient.field in
lemma separable_map {S} [CommRing S] [Nontrivial S] (f : F →+* S) {p : F[X]} :
    (p.map f).Separable ↔ p.Separable := by
  refine ⟨fun H ↦ ?_, fun H ↦ H.map⟩
  obtain ⟨m, hm⟩ := Ideal.exists_maximal S
  have := Separable.map H (f := Ideal.Quotient.mk m)
  rwa [map_map, separable_def, derivative_map, isCoprime_map] at this

[riccardobrasca]

Thanks!

bors +

[mathlib-bors]

Did you mean "r+"?

[riccardobrasca]

Did you mean "r+"?

Almost, but thanks bors!!

bors d+

[mathlib-bors]

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

[erdOne]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style