liftRingHom_apply — Mathlib

English

For a Ring hom φ between polynomial rings, the lifted RatFunc equals the ratio of mapped numerator and denominator: liftRingHom φ hφ f = φ f.num / φ f.denom.

Русский

Для кольцевого гомоморфизма φ между кольцами многочленыx выполняется то же самое: liftRingHom φ hφ f = φ f.num / φ f.denom.

LaTeX

$$$\\operatorname{liftRingHom}(\\phi, h\\phi)(f) = \\dfrac{\\phi(f\\text{.num})}{\\phi(f\\text{.denom})}$$$

Lean4

theorem liftRingHom_apply {L : Type*} [Field L] (φ : K[X] →+* L) (hφ : K[X]⁰ ≤ L⁰.comap φ) (f : RatFunc K) :
    liftRingHom φ hφ f = φ f.num / φ f.denom :=
  liftMonoidWithZeroHom_apply _ hφ _

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