homothety_one_half — Mathlib

English

With a field k, the homothety with center a and ratio 1/2 equals the midpoint.

Русский

В поле k гомотетия с центром a и коэффициентом 1/2 равна середине между a и b.

LaTeX

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

Lean4

theorem homothety_one_half {k : Type*} {V P : Type*} [Field k] [CharZero k] [AddCommGroup V] [Module k V]
    [AddTorsor V P] (a b : P) : homothety a (1 / 2 : k) b = midpoint k a b := by rw [one_div, homothety_inv_two]

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