map — Mathlib

English

If p is separable over R and f: R →+* S is a ring homomorphism, then the image p.map f is separable over S.

Русский

Если p разделим над R и f: R →+* S — гомоморфизм колец, то полином p.map f разделим над S.

LaTeX

$$$\\operatorname{Separable}(p) \\Rightarrow \\operatorname{Separable}(p\\map f)$$$

Lean4

theorem map {p : R[X]} (h : p.Separable) {f : R →+* S} : (p.map f).Separable :=
  let ⟨a, b, H⟩ := h
  ⟨a.map f, b.map f, by
    rw [derivative_map, ← Polynomial.map_mul, ← Polynomial.map_mul, ← Polynomial.map_add, H, Polynomial.map_one]⟩

Похожие утверждения