English
An additional equality criterion for RatFunc.mk: given nonzero q, q', equality of RatFunc mk's is equivalent to a cross-multiplication relation in polynomials.
Русский
Дополнительное условие равенства RatFunc.mk: при q,q' ≠ 0 равенство RatFunc mk эквивалентно перекрестному умножению полиномов.
LaTeX
$$$\\forall p,q,p',q' \\; (hq:hq' ≠ 0) \\, ,\\; \\text{Eq}(\\text{RatFunc.mk}\\, p\\, q) (\\text{RatFunc.mk}\\, p'\\, q') \\iff p \\cdot q' = p'\\cdot q$$$
Lean4
theorem mk_eq_mk {p q p' q' : K[X]} (hq : q ≠ 0) (hq' : q' ≠ 0) : RatFunc.mk p q = RatFunc.mk p' q' ↔ p * q' = p' * q :=
by
rw [mk_def_of_ne _ hq, mk_def_of_ne _ hq', ofFractionRing_injective.eq_iff, IsLocalization.mk'_eq_iff_eq',
(IsFractionRing.injective K[X] (FractionRing K[X])).eq_iff]
