homothety_eq_lineMap

Mathlib.LinearAlgebra.AffineSpace.AffineMap

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

English

For all c,r,p, the homothety at c with factor r equals the line map with the same parameters.

Русский

Гомотетия с центром c и коэффициентом r равна линейному отображению по той же линии.

LaTeX

$$$\operatorname{homothety}(c,r)(p) = \operatorname{lineMap}(c,p,r)$$$

Lean4

theorem homothety_eq_lineMap (c : P1) (r : k) (p : P1) : homothety c r p = lineMap c p r :=
  rfl

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

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

Разделы

Аффилиация

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