mk'_eq_mk' — Mathlib

English

For any submodule p and element x ∈ M, (Quot.mk x) equals mk x; i.e., the quotient constructor aligns with the canonical coset map.

Русский

Для любого подмодуля p и элемента x ∈ M имеет место равенство Quot.mk x = mk x; конструктор фактор-модуля согласован с каноническим отображением косета.

LaTeX

$$$ (\Quot.mk _ x) = mk x. $$$

Lean4

theorem mk'_eq_mk' {p : Submodule R M} (x : M) : @Quotient.mk' _ (quotientRel p) x = mk x :=
  rfl

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