of_isLocalization — Mathlib

English

If reg is IsSMulRegular on R and p localization exists, then IsSMulRegular on S holds for algebraMap.

Русский

Если reg является IsSMulRegular на R и существует локализация p, тогда IsSMulRegular на S сохраняется для алгебраического отображения.

LaTeX

$$$IsSMulRegular(R,x) \\Rightarrow IsSMulRegular(S, \\text{algebraMap}(R,S)(x))$$$

Lean4

theorem of_isLocalization {x : R} (reg : IsSMulRegular R x) : IsSMulRegular S (algebraMap R S x) :=
  reg.of_isLocalizedModule S p (Algebra.linearMap R S)

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