quotEquivOfEq_mk — Mathlib

English

If h : p = p', then the canonical equivalence sends mk x to mk x (i.e., it acts as the identity on representatives).

Русский

При наличии h : p = p' каноническое эквивалентное отображение отправляет mk x в mk x (ведет себя как тождественное отображение на представителей).

LaTeX

$$$\text{quotEquivOfEq}_p^{p'}(h)(\mathrm{mk}(x)) = \mathrm{mk}(x)$$$

Lean4

@[simp]
theorem quotEquivOfEq_mk (h : p = p') (x : M) :
    Submodule.quotEquivOfEq p p' h (Submodule.Quotient.mk x) = (Submodule.Quotient.mk x) :=
  rfl

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