English
If q ≠ 0, then the map φ respects division by q: map φ hφ (p/q) = φ(p)/φ(q) provided q is nonzero in the domain.
Русский
Если q ≠ 0, то отображение φ сохраняет деление на q: map φ hφ (p/q) = φ(p)/φ(q).
LaTeX
$$$\\text{If } q \\neq 0,\\; map(φ,hφ)(\\frac{p}{q}) = \\frac{φ(p)}{φ(q)}$$$
Lean4
theorem map_apply_div_ne_zero {R F : Type*} [CommRing R] [IsDomain R] [FunLike F K[X] R[X]] [MonoidHomClass F K[X] R[X]]
(φ : F) (hφ : K[X]⁰ ≤ R[X]⁰.comap φ) (p q : K[X]) (hq : q ≠ 0) :
map φ hφ (algebraMap _ _ p / algebraMap _ _ q) = algebraMap _ _ (φ p) / algebraMap _ _ (φ q) :=
by
have hq' : φ q ≠ 0 := nonZeroDivisors.ne_zero (hφ (mem_nonZeroDivisors_iff_ne_zero.mpr hq))
simp only [← mk_eq_div, mk_eq_localization_mk _ hq, map_apply_ofFractionRing_mk, mk_eq_localization_mk _ hq']
