map_subtype_top — Mathlib

English

The image of the top submodule under p.subtype equals p itself.

Русский

Образ верхнего подмодуля под действием p.subtype равен самому p.

LaTeX

$$$$ \operatorname{map}(p.\mathrm{subtype}, \top) = p $$$$

Lean4

/-- Under the canonical linear map from a submodule `p` to the ambient space `M`, the image of the
maximal submodule of `p` is just `p`. -/
theorem map_subtype_top : map p.subtype (⊤ : Submodule R p) = p := by simp

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