liftAlgHom_apply_div — Mathlib

English

For polynomials p, q, liftAlgHom φ hφ (algebraMap p / algebraMap q) = φ(p) / φ(q).

Русский

Для полиномов p, q: liftAlgHom φ hφ (алгебраMap p / алгебраMap q) = φ(p) / φ(q).

LaTeX

$$$\text{liftAlgHom}(\varphi,h_\varphi)\big(\dfrac{\text{algebraMap } p}{\text{algebraMap } q}\big) = \dfrac{\varphi(p)}{\varphi(q)}$$$

Lean4

theorem liftAlgHom_apply_div (p q : K[X]) : liftAlgHom φ hφ (algebraMap _ _ p / algebraMap _ _ q) = φ p / φ q :=
  liftMonoidWithZeroHom_apply_div _ hφ _ _

Похожие утверждения