const_apply

Mathlib.LinearAlgebra.Pi

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

English

The constant linear map sends every element to the constant function at that element.

Русский

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

LaTeX

$$const : M2 →ₗ[R] (ι → M2)$$

Lean4

@[simp]
theorem const_apply (x : M₂) : LinearMap.const (R := R) x = Function.const ι x :=
  rfl

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

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

Разделы

Аффилиация

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