liftAlgHom_apply_ofFractionRing_mk

English

For any polynomial p, d with certain non-zero-divisor conditions, liftAlgHom sends the fraction of p and d to φ(p)/φ(d).

Русский

Для любых p и d, удовлетворяющих условиям, liftAlgHom отображает долю p/d в φ(p)/φ(d).

LaTeX

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

Lean4

theorem liftAlgHom_apply_ofFractionRing_mk (n : K[X]) (d : K[X]⁰) :
    liftAlgHom φ hφ (ofFractionRing (Localization.mk n d)) = φ n / φ d :=
  liftMonoidWithZeroHom_apply_ofFractionRing_mk _ hφ _ _

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