const

Mathlib.LinearAlgebra.Pi

URI: https://scilib.ai/kg/mathlib#LinearMap.const

English

The projection operator followed by pi is the identity on the target product module.

Русский

Оператор проекции, применённый к Pi, возвращает исходный элемент на произведении модулей.

LaTeX

$$proj_pi$$

Lean4

/-- The constant linear map, taking `x` to `Function.const ι x`. -/
def const : M₂ →ₗ[R] (ι → M₂) :=
  pi fun _ ↦ .id

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

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

Разделы

Аффилиация

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