isLocalization_C_mk' — Mathlib

English

For a localization S of R away from r, the canonical image of C with mk' meets the localized C-maps: C(IsLocalization.mk' S a m) = mk' (MvPolynomial σ S) (C a) ...

Русский

Для локализации S от элемента r каноническое изображение C через mk' удовлетворяет локализации: C(IsLocalization.mk' S a m) = mk'(MvPolynomial σ S)(C a)…

LaTeX

$$C(IsLocalization.mk' S a m) = IsLocalization.mk'(MvPolynomial σ S) (C a) ⟨C m, Submonoid.mem_map_of_mem C m.property⟩$$

Lean4

theorem isLocalization_C_mk' (a : R) (m : M) :
    C (IsLocalization.mk' S a m) =
      IsLocalization.mk' (MvPolynomial σ S) (C (σ := σ) a) ⟨C m, Submonoid.mem_map_of_mem C m.property⟩ :=
  by simp_rw [IsLocalization.eq_mk'_iff_mul_eq, algebraMap_def, map_C, ← map_mul, IsLocalization.mk'_spec]

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