LocalizedModule — Mathlib

English

The localized module LocalizedModule S M is defined as the quotient of M × S by the relation r.

Русский

Локализованный модуль LocalizedModule S M определяется как фактор-множество (M × S)/~ по отношению r.

LaTeX

$$$\\text{LocalizedModule}(S,M) = (M \\times S)/\\sim_{r}$.$$

Lean4

/-- If `S` is a multiplicative subset of a ring `R` and `M` an `R`-module, then
we can localize `M` by `S`.
-/
def _root_.LocalizedModule : Type max u v :=
  Quotient (r.setoid S M)

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