toSubmodule_injective — Mathlib

English

The map sending a homogeneous submodule to its underlying submodule is injective.

Русский

Отображение от однородного подмодуля к его базовому подмодулю инъективно.

LaTeX

$$$$ \text{toSubmodule}: \text{HomogeneousSubmodule } 𝒜 \ℳ \to \text{Submodule } A M \quad \text{is injective}. $$$$

Lean4

theorem toSubmodule_injective :
    Function.Injective (HomogeneousSubmodule.toSubmodule : HomogeneousSubmodule 𝒜 ℳ → Submodule A M) :=
  fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ fun (h : x = y) ↦ by simp [h]

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