lineMap_apply_ring'

Mathlib.LinearAlgebra.AffineSpace.AffineMap

URI: https://scilib.ai/kg/mathlib#AffineMap.lineMap_apply_ring'

English

LineMap with v added to p yields the parametrization of the line in direction v from p.

Русский

LineMap с добавлением вектора v к p задаёт параметризацию прямой в направлении v от p.

LaTeX

$$$ lineMap(p, p+\! v) (c) = c \cdot v + p $$$

Lean4

theorem lineMap_apply_ring' (a b c : k) : lineMap a b c = c * (b - a) + a :=
  rfl

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

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

Разделы

Аффилиация

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