quotEquivOfEqBot_apply_mk — Mathlib

English

Let p be the zero submodule of a module M over a ring R. Then the natural isomorphism between M/p and M is the identity on representatives: for every x in M, the image of x modulo p is x.

Русский

Пусть p — нулевой подмодуль M над кольцом R. Тогда естественный изоморфизм между M/p и M действует как тождественный на представителях: для каждого x ∈ M образ x mod p равен x.

LaTeX

$$$\forall p\subseteq M,\; p=\{0\} \Rightarrow \forall x\in M,\; \varphi_p([x]) = x,$$$

Lean4

@[simp]
theorem quotEquivOfEqBot_apply_mk (hp : p = ⊥) (x : M) : p.quotEquivOfEqBot hp (Quotient.mk x) = x :=
  rfl

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