homothety_invOf_two — Mathlib

English

In a commutative ring with invertible 2, the homothety with center a and ratio 2^{-1} maps b to the midpoint of a and b.

Русский

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

LaTeX

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

Lean4

theorem homothety_invOf_two {R : Type*} {V P : Type*} [CommRing R] [Invertible (2 : R)] [AddCommGroup V] [Module R V]
    [AddTorsor V P] (a b : P) : homothety a (⅟2 : R) b = midpoint R a b :=
  rfl

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