const_linear

Mathlib.LinearAlgebra.AffineSpace.AffineMap

URI: https://scilib.ai/kg/mathlib#AffineMap.const_linear

English

The coercion of the constant affine map to a function is the constant function that always returns p.

Русский

Приведение константного аффинного отображения к функции даёт константную функцию, возвращающую p.

LaTeX

$$const k P1 p q = p for all q$$

Lean4

@[simp]
theorem const_linear (p : P2) : (const k P1 p).linear = 0 :=
  rfl

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

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

Разделы

Аффилиация

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