restrictScalars_self

Mathlib.Algebra.Module.Submodule.RestrictScalars

URI: https://scilib.ai/kg/mathlib#Submodule.restrictScalars_self

English

The map Submodule.restrictScalars with respect to S is injective.

Русский

Гомоморфизм Submodule.restrictScalars относительно S инъективен.

LaTeX

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

Lean4

@[simp]
theorem restrictScalars_self (V : Submodule R M) : V.restrictScalars R = V :=
  SetLike.coe_injective rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru