coe_toSubMulAction — Mathlib

English

Let p be a submodule of M. The underlying set of p obtained via the SubMulAction construction coincides with p itself, i.e., the set representing p is exactly p.

Русский

Пусть p — подмодуль множества M. Множество, представляющее p через конструкцию SubMulAction, совпадает с самим p.

LaTeX

$$$ (p^{\\mathrm{toSubMulAction}} : \\mathrm{Set} M) = p $$$

Lean4

@[simp]
theorem coe_toSubMulAction (p : Submodule R M) : (p.toSubMulAction : Set M) = p :=
  rfl

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