algebraMap_isUnit_iff — Mathlib

English

In Away, an element y maps to a unit precisely when y divides some power of x.

Русский

В Away отображение элемента y в единицу точно тогда, когда y делит некоторую степень x.

LaTeX

$$IsLocalization.Away.algebraMap_isUnit_iff x {y : R}$$

Lean4

theorem algebraMap_isUnit_iff {y : R} : IsUnit (algebraMap R S y) ↔ ∃ n, y ∣ x ^ n :=
  (IsLocalization.algebraMap_isUnit_iff <| .powers x).trans <| by simp [Submonoid.mem_powers_iff]

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