localization_base — Mathlib

English

Localization at a single element preserves unramifiedness: Away r gives an unramified extension.

Русский

Локализация по одному элементу сохраняет неразветвленность: Away r дает неразветвленное расширение.

LaTeX

$$$[\text{IsLocalization.Away } r\; A] \Rightarrow [\text{Unramified } R \; A]$$$

Lean4

/-- This actually does not need the localization instance, and is stated here again for
consistency. See `Algebra.FormallyUnramified.of_comp` instead.

The intended use is for copying proofs between `Formally{Unramified, Smooth, Etale}`
without the need to change anything (including removing redundant arguments). -/
@[nolint unusedArguments]
theorem localization_base [FormallyUnramified R Sₘ] : FormallyUnramified Rₘ Sₘ :=
  FormallyUnramified.of_comp R Rₘ Sₘ

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