map_id — Mathlib

English

If l: M → N is injective, then its localized map map S l is injective.

Русский

Если l: M → N инъективно, то локализованное отображение map S l также инъективно.

LaTeX

$$$\\text{map}_S(l) \\text{ is injective if } l \\text{ is injective}$$$

Lean4

@[simp]
theorem map_id : LocalizedModule.map S (.id (R := R) (M := M)) = LinearMap.id :=
  LinearMap.ext fun x ↦ LinearMap.congr_fun (IsLocalizedModule.map_id S (mkLinearMap S M)) x

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