lineMap_inv_two — Mathlib

English

In a division ring setting, the line map between a and b at parameter 2^{-1} equals the midpoint of a and b.

Русский

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

LaTeX

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

Lean4

theorem lineMap_inv_two {R : Type*} {V P : Type*} [DivisionRing R] [CharZero R] [AddCommGroup V] [Module R V]
    [AddTorsor V P] (a b : P) : lineMap a b (2⁻¹ : R) = midpoint R a b :=
  rfl

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