top

Mathlib.LinearAlgebra.Projection

URI: https://scilib.ai/kg/mathlib#LinearMap.IsProj.top

English

m equals the top submodule iff f equals the identity map.

Русский

Подмодуль m равен верхнему эквиваленту тогда и только тогда, когда f = id.

LaTeX

$$$m = \top \;\iff\; f = \mathrm{id}.$$$

Lean4

protected theorem top : IsProj (⊤ : Submodule S M) (id (R := S)) :=
  ⟨fun _ ↦ trivial, fun _ ↦ congrFun rfl⟩

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

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

Разделы

Аффилиация

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