isUnit_to_basicOpen_self — Mathlib

English

For any f in R, the element corresponding to f in the basic open is a unit in the localization at that basic open.

Русский

Для любого f в R соответствующий элемент в базовом открытом множестве является единицей в локализации на этом открытом.

LaTeX

$$$ IsUnit\\left( toOpen\_R(\\operatorname{basicOpen}(f)) f \\right) $$$

Lean4

theorem isUnit_to_basicOpen_self (f : R) : IsUnit (toOpen R (PrimeSpectrum.basicOpen f) f) :=
  isUnit_of_mul_eq_one _ (const R 1 f (PrimeSpectrum.basicOpen f) fun _ => id) <| by rw [toOpen_eq_const, const_mul_rev]

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