English
For polynomials p,q, RatFunc.mk p q equals the division of algebra maps: (algebraMap p)/(algebraMap q) in RatFunc.
Русский
Для многочленов p,q RatFunc.mk p q эквивалентно делению algebraMap p на algebraMap q.
LaTeX
$$$\\text{RatFunc}.mk(p,q) = \\frac{\\text{algebraMap } p}{\\text{algebraMap } q}$$$
Lean4
@[simp]
theorem map_apply_div {R F : Type*} [CommRing R] [IsDomain R] [FunLike F K[X] R[X]] [MonoidWithZeroHomClass F K[X] R[X]]
(φ : F) (hφ : K[X]⁰ ≤ R[X]⁰.comap φ) (p q : K[X]) :
map φ hφ (algebraMap _ _ p / algebraMap _ _ q) = algebraMap _ _ (φ p) / algebraMap _ _ (φ q) :=
by
rcases eq_or_ne q 0 with (rfl | hq)
· have : (0 : RatFunc K) = algebraMap K[X] _ 0 / algebraMap K[X] _ 1 := by simp
rw [map_zero, map_zero, map_zero, div_zero, div_zero, this, map_apply_div_ne_zero, map_one, map_one, div_one,
map_zero, map_zero]
exact one_ne_zero
exact map_apply_div_ne_zero _ _ _ _ hq
