liftMonoidWithZeroHom_apply_ofFractionRing_mk

English

For φ and hφ as above and n ∈ R[X], d ∈ R[X]^0, applyinglift to the fraction Localization.mk n d yields φ(n)/φ(d) in the target.

Русский

При указанных φ и hφ и элемента n ∈ R[X], d ∈ R[X]^0 отображение подействует на Localization.mk n d и дадут φ(n)/φ(d).

LaTeX

$$$\mathrm{liftMonoidWithZeroHom}\,φ\,hφ\,(\mathrm{ofFractionRing}(\mathrm{Localization.mk}(n,d))) = φ(n)/φ(d)$$$

Lean4

theorem liftMonoidWithZeroHom_apply_ofFractionRing_mk (φ : R[X] →*₀ G₀) (hφ : R[X]⁰ ≤ G₀⁰.comap φ) (n : R[X])
    (d : R[X]⁰) : liftMonoidWithZeroHom φ hφ (ofFractionRing (Localization.mk n d)) = φ n / φ d :=
  liftOn_ofFractionRing_mk _ _ _ _

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