mk — Mathlib · SciLib

English

The map sending x ∈ M and y ∈ S to the localization class is the mk construction.

Русский

Отображение, отправляющее x ∈ M и y ∈ S в класс локализации, задаётся как mk.

LaTeX

$$$ (x,y) \mapsto \mathrm{Localization.mk}(x,y) $$$

Lean4

/-- Given a `CommMonoid` `M` and submonoid `S`, `mk` sends `x : M`, `y ∈ S` to the equivalence
class of `(x, y)` in the localization of `M` at `S`. -/
@[to_additive /-- Given an `AddCommMonoid` `M` and submonoid `S`, `mk` sends `x : M`, `y ∈ S` to
    the equivalence class of `(x, y)` in the localization of `M` at `S`. -/
    ]
def mk (x : M) (y : S) : Localization S :=
  x /ₒ y

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