mk_one' — Mathlib

English

For polynomials p,q,p',q' with q,q' ≠ 0, RatFunc.mk p q = RatFunc.mk p' q' iff p·q' = p'·q.

Русский

Для многочленов p,q,p',q' с q,q' ≠ 0, RatFunc.mk p q = RatFunc.mk p' q' тогда и только тогда, когда p·q' = p'·q.

LaTeX

$$$\\text{RatFunc.mk}\\, p\\, q = \\text{RatFunc.mk}\\, p'\\, q' \\iff p \\cdot q' = p'\\cdot q$$$

Lean4

theorem mk_one' (p : K[X]) : RatFunc.mk p 1 = ofFractionRing (algebraMap _ _ p) := by
  rw [← IsLocalization.mk'_one (M := K[X]⁰) (FractionRing K[X]) p, ← mk_coe_def, Submonoid.coe_one]

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