English
An equivalence between IsUnit of the denominator and integrality in the localization sense.
Русский
Эквивалентность единичности знаменателя и интегрированности в локализационном смысле.
LaTeX
$$$\\text{IsUnit}(\\mathrm{den}_A(x)) \\iff \\text{IsLocalization.IsInteger}_A(x)$$$
Lean4
theorem isUnit_den_iff (x : K) : IsUnit (den A x : A) ↔ IsLocalization.IsInteger A x
where
mp := isInteger_of_isUnit_den
mpr
h := by
have ⟨v, h⟩ := h
apply IsRelPrime.isUnit_of_dvd (num_den_reduced A x).symm
use v
apply_fun algebraMap A K
· simp only [map_mul, h]
rw [mul_comm, ← div_eq_iff]
· simp only [mk'_num_den']
intro h
replace h : algebraMap A K (den A x : A) = algebraMap A K 0 := by convert h; simp
exact nonZeroDivisors.coe_ne_zero _ <| FaithfulSMul.algebraMap_injective A K h
exact FaithfulSMul.algebraMap_injective A K
