English
In the refined form, the lift preserves division at the level of polynomials: liftRingHom φ hφ (algebraMap K[X] p) / liftRingHom φ hφ (algebraMap K[X] q) = φ(p) / φ(q) for p, q ∈ K[X].
Русский
В улучшенной форме подъем сохраняет деление на уровне многочленов: liftRingHom φ hφ(алгебраMap p) / liftRingHom φ hφ(алгебраMap q) = φ(p) / φ(q), для p, q ∈ K[X].
LaTeX
$$$ \dfrac{\operatorname{liftRingHom}(\varphi, h_\varphi)(\text{algebraMap } p)}{\operatorname{liftRingHom}(\varphi, h_\varphi)(\text{algebraMap } q)} = \dfrac{\varphi(p)}{\varphi(q)} \quad(p,q \in K[X])$$$
Lean4
@[simp]
theorem liftRingHom_apply_div' {L : Type*} [Field L] (φ : K[X] →+* L) (hφ : K[X]⁰ ≤ L⁰.comap φ) (p q : K[X]) :
liftRingHom φ hφ (algebraMap _ _ p) / liftRingHom φ hφ (algebraMap _ _ q) = φ p / φ q :=
liftMonoidWithZeroHom_apply_div' _ hφ _ _
