mk

Mathlib.Algebra.Module.LocalizedModule.Basic

URI: https://scilib.ai/kg/mathlib#LocalizedModule.mk

English

The canonical map sends a pair (m,s) to its class in the localization, i.e., (m,s) ↦ [(m,s)].

Русский

Каноническое отображение отправляет пару (m,s) в её класс в локализации, т.е. (m,s) ↦ [(m,s)].

LaTeX

$$$\\text{mk}(m,s) = [(m,s)].$$$

Lean4

/-- The canonical map sending `(m, s) ↦ m/s` -/
def mk (m : M) (s : S) : LocalizedModule S M :=
  Quotient.mk' ⟨m, s⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru