English
For a suitable map φ and RatFunc f, the image under φ equals the ratio of the mapped numerator and mapped denominator: map φ f = φ(num(f)) / φ(denom(f)).
Русский
Для надлежащего отображения φ и рациональной функции f образ выполняется так: map φ f = φ(num(f)) / φ(denom(f)).
LaTeX
$$$\\operatorname{map}(\\phi)(f) = \\dfrac{\\phi(\\mathrm{num}(f))}{\\phi(\\mathrm{denom}(f))}$$$
Lean4
theorem map_apply {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 φ) (f : RatFunc K) : map φ hφ f = algebraMap _ _ (φ f.num) / algebraMap _ _ (φ f.denom) :=
by
rw [← num_div_denom f, map_apply_div_ne_zero, num_div_denom f]
exact denom_ne_zero _
