QuotSMulTop — Mathlib

English

An abbreviation for the quotient M modulo rM, i.e., the quotient of M by the submodule generated by r.

Русский

Укорочение M по подмодулю rM, то есть фактор-модуль M / (rM).

LaTeX

$$$$ \text{QuotSMulTop}(r,M) = M / (r\cdot M) $$.$$

Lean4

/-- An abbreviation for `M⧸rM` that keeps us from having to write
`(⊤ : Submodule R M)` over and over to satisfy the typechecker. -/
abbrev QuotSMulTop :=
  M ⧸ r • (⊤ : Submodule R M)

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