liftAlgHom_apply_div' — Mathlib

English

There is a formula for liftAlgHom applied to the fraction given by a numerator n and denominator d in the fraction ring, yielding φ(n)/φ(d).

Русский

Существует формула для применения liftAlgHom к дроби n/d в дробном кольце, дающая φ(n)/φ(d).

LaTeX

$$$\text{liftAlgHom}(\varphi,h_\varphi)\big(\text{ofFractionRing} (\text{Localization.mk } n d)\big) = \dfrac{\varphi(n)}{\varphi(d)}$$$

Lean4

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

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