restrictScalars_injective — Mathlib

English

Restriction preserves injectivity: the restricted map is injective iff the original is.

Русский

Ограничение сохраняет инъективность: ограниченное отображение инъективно тогда и только тогда, когда исходное отображение инъективно.

LaTeX

$$$$ \\operatorname{restrictScalars}(S,V_1) = \\operatorname{restrictScalars}(S,V_2) \\iff V_1 = V_2. $$$$

Lean4

theorem restrictScalars_injective : Function.Injective (restrictScalars S : Submodule R M → Submodule S M) :=
  fun _ _ h => ext <| Set.ext_iff.1 (SetLike.ext'_iff.1 h :)

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