map_divByMonic — Mathlib

English

For a ring hom f and monic q, the map of the quotient equals the quotient of the maps: map f (p /ₘ q) = map f p /ₘ map f q.

Русский

При гомоморфизме f и мономическом q отображение сохраняет частное: map f (p /ₘ q) = map f p /ₘ map f q.

LaTeX

$$$$ \\operatorname{map} f \\left(p /ₘ q\\right) = \\operatorname{map} f(p) /ₘ \\operatorname{map} f(q). $$$$

Lean4

theorem map_divByMonic [Ring S] (f : R →+* S) (hq : Monic q) : (p /ₘ q).map f = p.map f /ₘ q.map f :=
  (map_mod_divByMonic f hq).1

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