homothety_zero

Mathlib.LinearAlgebra.AffineSpace.AffineMap

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

English

The homothety with scale factor 0 is the constant map sending every point to the center c.

Русский

Гомотетия с коэффициентом 0 — константное отображение, отправляющее каждую точку в центр c.

LaTeX

$$$\operatorname{homothety}(c,0) = \text{const}_{c}$$$

Lean4

@[simp]
theorem homothety_zero (c : P1) : homothety c (0 : k) = const k P1 c :=
  by
  ext p
  simp [homothety_apply]

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

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

Разделы

Аффилиация

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