hasQuotient — Mathlib

English

The quotient M/p is the set of equivalence classes under the relation x ~ y iff x − y ∈ p.

Русский

Фактор-модуль M/p — множество классов эквивалентности по отношению x ~ y ⇔ x − y ∈ p.

LaTeX

$$$M/p \cong \{\text{equivalence classes of } M \text{ under } \sim\}, \; x \sim y \Leftrightarrow x-y \in p.$$$

Lean4

/-- The quotient of a module `M` by a submodule `p ⊆ M`. -/
instance hasQuotient : HasQuotient M (Submodule R M) :=
  ⟨fun p => Quotient (quotientRel p)⟩

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