homothety_inv_two — Mathlib

English

For a field k, the homothety with center a and ratio 2^{-1} maps b to the midpoint of a and b.

Русский

Для поля k гомотетия с центром a и коэффициентом 2^{-1} переводит b в середину между a и b.

LaTeX

$$$ \operatorname{homothety}_k(a, 2^{-1}) b = \operatorname{midpoint}_k a b $$$

Lean4

theorem homothety_inv_two {k : Type*} {V P : Type*} [Field k] [CharZero k] [AddCommGroup V] [Module k V] [AddTorsor V P]
    (a b : P) : homothety a (2⁻¹ : k) b = midpoint k a b :=
  rfl

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