invSubmonoid — Mathlib

English

In a localization S of R at M, the invSubmonoid is the distinguished submonoid of S consisting of elements that appear as 1/x with x ∈ M.

Русский

В локализации S кольца R при M, invSubmonoid — это особый подмоноид S, состоящий из элементов вида 1/x при x∈M.

LaTeX

$$$\operatorname{invSubmonoid}(M,S) = \{ \tfrac{1}{x} \mid x \in M \} \subseteq S$ (as a submonoid)$$

Lean4

/-- The submonoid of `S = M⁻¹R` consisting of `{ 1 / x | x ∈ M }`. -/
def invSubmonoid : Submonoid S :=
  (M.map (algebraMap R S)).leftInv

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