English
Let φ be a monoid-with-zero homomorphism between polynomial rings into a commutative group with zero L, and hφ a lattice-theoretic condition. For polynomials p,q with q ≠ 0, lifting through φ preserves the division in the target: lift φ hφ (p/q) = φ(p)/φ(q).
Русский
Пусть φ — морфизм моноида с нулём между кольцами многочленов в коммутативную группу L с нулём, и hφ удовлетворяет соответствующему условию решётки. При q ≠ 0 отношение p/q сохраняется после подъёма: lift φ hφ (p/q) = φ(p)/φ(q).
LaTeX
$$$ liftMonoidWithZeroHom\\; φ\\; hφ\\; (p/q) = φ(p)/φ(q) $$$
Lean4
@[simp]
theorem liftMonoidWithZeroHom_apply_div' {L : Type*} [CommGroupWithZero L] (φ : MonoidWithZeroHom K[X] L)
(hφ : K[X]⁰ ≤ L⁰.comap φ) (p q : K[X]) :
liftMonoidWithZeroHom φ hφ (algebraMap _ _ p) / liftMonoidWithZeroHom φ hφ (algebraMap _ _ q) = φ p / φ q := by
rw [← map_div₀, liftMonoidWithZeroHom_apply_div]
