coe_homothetyUnitsMulHom_apply_symm

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

URI: https://scilib.ai/kg/mathlib#AffineEquiv.coe_homothetyUnitsMulHom_apply_symm

← MathLib Explorer

English

The inverse of the homothety action by t is the homothety by t^{-1}.

Русский

Обратное к действию гомотетии единицы t задаётся гомотенией по t^{-1}.

LaTeX

$$((homothetyUnitsMulHom p t).symm) = AffineMap.homothety p (t^{-1})$$

Lean4

@[simp]
theorem coe_homothetyUnitsMulHom_apply_symm (p : P) (t : Rˣ) :
    ((homothetyUnitsMulHom p t).symm : P → P) = AffineMap.homothety p (↑t⁻¹ : R) :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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