bot

Mathlib.LinearAlgebra.Projection

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

English

The bottom submodule with the zero endomorphism is a projection.

Русский

Нижнее подпространство с нулевым отображением является проекцией.

LaTeX

$$IsProj(⊥,0) holds.$$

Lean4

protected theorem bot : IsProj (⊥ : Submodule S M) (0 : M →ₗ[S] M) :=
  ⟨congrFun rfl, by simp only [mem_bot, zero_apply, forall_eq]⟩

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

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

Разделы

Аффилиация

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