of_isLocalization_Away — Mathlib

English

Localization at a single element is étale.

Русский

Локализация по одному элементу является étale.

LaTeX

$$$\forall r\in R,\; [\text{IsLocalization.Away } r \; A] \Rightarrow \text{Etale } R A$$$

Lean4

/-- Localization at an element is étale. -/
theorem of_isLocalization_Away (r : R) [IsLocalization.Away r A] : Etale R A
    where
  formallyEtale := Algebra.FormallyEtale.of_isLocalization (Submonoid.powers r)
  finitePresentation := IsLocalization.Away.finitePresentation r

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