mem_invtSubmodule_iff_mapsTo

Mathlib.Algebra.Module.Submodule.Invariant

URI: https://scilib.ai/kg/mathlib#Module.End.mem_invtSubmodule_iff_mapsTo

← MathLib Explorer

English

An invariant submodule is exactly those p such that maps f p to p.

Русский

Инвариантный подмодуль — это те p, для которых f(p) ⊆ p.

LaTeX

$$mem_invtSubmodule_iff_mapsTo: p ∈ f.invtSubmodule ↔ Set.MapsTo f p p$$

Lean4

/-- `p` is `f` invariant if and only if `Set.MapsTo f p p`. -/
theorem mem_invtSubmodule_iff_mapsTo {p : Submodule R M} : p ∈ f.invtSubmodule ↔ Set.MapsTo f p p :=
  Iff.rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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