liftOn_ofFractionRing_mk — Mathlib

English

A duplicate statement ensuring LiftOn for Fraction Ring MK holds similarly to the previous item.

Русский

Дубликат утверждения о LiftOn для Fraction Ring MK аналогично предыдущему.

LaTeX

$$$\\text{LiftOn}(\\text{ofFractionRing}(\\text{Localization.mk}\\, n\, d)) = f(n,d)$$$

Lean4

theorem liftOn_ofFractionRing_mk {P : Sort v} (n : K[X]) (d : K[X]⁰) (f : K[X] → K[X] → P)
    (H : ∀ {p q p' q'} (_hq : q ∈ K[X]⁰) (_hq' : q' ∈ K[X]⁰), q' * p = q * p' → f p q = f p' q') :
    RatFunc.liftOn (ofFractionRing (Localization.mk n d)) f @H = f n d :=
  by
  rw [RatFunc.liftOn]
  exact Localization.liftOn_mk _ _ _ _

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