mk_eq_mk' — Mathlib

English

For f ∈ K[X] and g ∈ K[X], with g ≠ 0, RatFunc.mk f g equals IsLocalization.mk' (RatFunc K) f with the witness that g is non-zero-divisor.

Русский

Для f,g ∈ K[X], g ≠ 0, RatFunc.mk f g равно IsLocalization.mk' (RatFunc K) f с свидетельством того, что g невзводимый.

LaTeX

$$$\text{RatFunc.mk } f g = \text{IsLocalization.mk'} (\text{RatFunc } K) f ⟨g, mem_nonZeroDivisors_iff_ne_zero.2 g \neq 0⟩$$$

Lean4

theorem mk_eq_mk' (f : Polynomial K) {g : Polynomial K} (hg : g ≠ 0) :
    RatFunc.mk f g = IsLocalization.mk' (RatFunc K) f ⟨g, mem_nonZeroDivisors_iff_ne_zero.2 hg⟩ := by
  simp only [mk_eq_div, IsFractionRing.mk'_eq_div]

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