homothety_apply_same

Mathlib.LinearAlgebra.AffineSpace.AffineMap

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

English

The linear part of homothety c r is r times the identity map.

Русский

Линейная часть гомотетии равна r на тождественному отображению.

LaTeX

$$$\big(\operatorname{homothety}(c,r)\big)^{\text{linear}} = r \cdot \mathrm{Id}$$$

Lean4

@[simp]
theorem homothety_apply_same (c : P1) (r : k) : homothety c r c = c :=
  lineMap_same_apply c r

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

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

Разделы

Аффилиация

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