map_units_map_submonoid — Mathlib

English

For a submonoid y ∈ M, algebraMap R S_m y is a unit in the localization S_m; hence y maps to a unit under the localization map.

Русский

Для элемента y ∈ M отображение algebraMap R S_m y является единицей в локализации S_m; следовательно, y отображается в единицу локализации.

LaTeX

$$$\forall y \,(y \in M) \Rightarrow IsUnit(\text{algebraMap } R S_m y)$$$

Lean4

theorem map_units_map_submonoid (y : M) : IsUnit (algebraMap R Sₘ y) :=
  by
  rw [IsScalarTower.algebraMap_apply _ S]
  exact
    IsLocalization.map_units Sₘ
      ⟨algebraMap R S y, Algebra.mem_algebraMapSubmonoid_of_mem y⟩
        -- can't be simp, as `S` only appears on the RHS

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