ordFrac_eq_ord — Mathlib

English

The quotient in ordFrac respects division for elements represented by non-zero divisors in the localization.

Русский

Часть ordFrac, связанная с делением, сохраняется для элементов, задаваемых через локализацию по ненулевым делителям.

LaTeX

$$ordFrac R (IsLocalization.mk' K a.1 b) = ordMonoidWithZeroHom R a / ordMonoidWithZeroHom R b$$

Lean4

theorem ordFrac_eq_ord (x : R) (hx : x ≠ 0) : ordFrac R (algebraMap R K x) = ordMonoidWithZeroHom R x :=
  by
  have := (FaithfulSMul.algebraMap_injective R K).isDomain
  refine (Submonoid.LocalizationMap.lift_eq ..).trans ?_
  simp [ordMonoidWithZeroHom, mem_nonZeroDivisors_iff_ne_zero.mpr hx]

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