English
The unit status of an element mapped from R to Localization.AtPrime I via algebraMap is controlled by membership in the prime complement; specifically, an element x ∈ R maps to a unit iff x lies in the prime complement I.primeCompl.
Русский
Единичность образа элемента x ∈ R в Localization.AtPrime I через algebraMap управляется принадлежностью x к primeCompl; то есть x мб единицей тогда и только тогда, когда x ∈ I.primeCompl.
LaTeX
$$$$ \text{isUnit_to_map_iff} : \mathrm{IsUnit}(\operatorname{algebraMap} R (Localization.AtPrime I)\ x) \iff x \in I.\text{primeCompl} $$$$
Lean4
theorem isUnit_mk'_iff (x : R) (y : I.primeCompl) : IsUnit (mk' S x y) ↔ x ∈ I.primeCompl :=
⟨fun h hx => mk'_mem_iff.mpr ((to_map_mem_maximal_iff S I x).mpr hx) h, fun h =>
isUnit_iff_exists_inv.mpr ⟨mk' S ↑y ⟨x, h⟩, mk'_mul_mk'_eq_one ⟨x, h⟩ y⟩⟩
