homothety_neg_one_apply — Mathlib

English

For any base point p in P1 and any scalar c from a commutative ring R', the homothety with factor -1 about c sends p to the point reflection of p about c; i.e., homothety(c, -1) p = pointReflection(R', c) p.

Русский

Для любой базовой точки p ∈ P1 и любого элемента c из кольца R' выполняется равенство: гомотетия с коэффициентом -1 относительно c отправляет p в отражение точки p относительно c; то есть homothety(c, -1) p = pointReflection(R', c) p.

LaTeX

$$$\mathrm{homothety}(c,-1)\,p = \mathrm{pointReflection}(R',c)\,p$$$

Lean4

theorem homothety_neg_one_apply (c p : P₁) : homothety c (-1 : R') p = pointReflection R' c p := by
  simp [homothety_apply, Equiv.pointReflection_apply]

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