restrictScalars_inj — Mathlib

English

Equivalence of equality after restriction characterizes equality of submodules.

Русский

Равенство после ограничения скаляров эквивалентно равенству подмодулей.

LaTeX

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

Lean4

@[simp]
theorem restrictScalars_inj {V₁ V₂ : Submodule R M} : restrictScalars S V₁ = restrictScalars S V₂ ↔ V₁ = V₂ :=
  (restrictScalars_injective S _ _).eq_iff

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