map_div — Mathlib

English

For any ring hom f, (p / q) maps to (p.map f) / (q.map f).

Русский

Для любого гомоморфизма колец, отображение дроби сохраняется: (p / q).map f = p.map f / q.map f.

LaTeX

$$$ (p / q)^{f} = p^{f} / q^{f} $$$

Lean4

theorem map_div [Field k] (f : R →+* k) : (p / q).map f = p.map f / q.map f := by
  if hq0 : q = 0 then simp [hq0]
  else
    rw [div_def, div_def, Polynomial.map_mul, map_divByMonic f (monic_mul_leadingCoeff_inv hq0), Polynomial.map_mul,
      map_C, leadingCoeff_map, map_inv₀]

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