map_injective — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem map_injective (l : M →ₗ[R] N) (hl : Function.Injective l) : Function.Injective (map S l) :=
  IsLocalizedModule.map_injective S (mkLinearMap S M) (mkLinearMap S N) l hl

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