map_id

Mathlib.Algebra.Module.Submodule.Map

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

English

For any submodule p of M, the image under the identity map is p itself: map id p = p.

Русский

Для любого подмодуля p ⊆ M образ под идентитичным отображением равен самому p: map id p = p.

LaTeX

$$$\\text{map} \\big( \\text{Id} : M \\to M \\big)\\; p = p$$

Lean4

@[simp]
theorem map_id : map (LinearMap.id : M →ₗ[R] M) p = p :=
  Submodule.ext fun a => by simp

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

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

Разделы

Аффилиация

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