homothety_one

Mathlib.LinearAlgebra.AffineSpace.AffineMap

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

English

For all c, r1, r2, p, we have homothety c (r1 r2) p = homothety c r1 (homothety c r2 p).

Русский

Для всех c, r1, r2, p выполняется: homothety c (r1 r2) p = homothety c r1 (homothety c r2 p).

LaTeX

$$$\operatorname{homothety}(c, r_1 r_2)(p) = \operatorname{homothety}(c, r_1)(\operatorname{homothety}(c, r_2)(p))$$$

Lean4

@[simp]
theorem homothety_one (c : P1) : homothety c (1 : k) = id k P1 :=
  by
  ext p
  simp [homothety_apply]

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

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

Разделы

Аффилиация

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