restrictScalars_mem

Mathlib.Algebra.Module.Submodule.RestrictScalars

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

English

Membership is preserved under restriction of scalars.

Русский

Членство сохраняется при ограничении скаляров.

LaTeX

$$$$ m \\in (V.\\restrictionScalars S) \\iff m \\in V. $$$$

Lean4

@[simp]
theorem restrictScalars_mem (V : Submodule R M) (m : M) : m ∈ V.restrictScalars S ↔ m ∈ V :=
  Iff.refl _

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

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

Разделы

Аффилиация

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