midpoint_unique — Mathlib

English

The midpoint does not depend on the ring: for any R', with invertible 2 and a compatible module structure, midpoint(R,x,y) = midpoint(R',x,y).

Русский

Середина не зависит от кольца: для любого R' с обратимым 2 и совместной структурой модуля, midpoint(R,x,y) = midpoint(R',x,y).

LaTeX

$$$ \\operatorname{midpoint}(R,x,y) = \\operatorname{midpoint}(R',x,y) $$$

Lean4

/-- `midpoint` does not depend on the ring `R`. -/
theorem midpoint_unique (R' : Type*) [Ring R'] [Invertible (2 : R')] [Module R' V] (x y : P) :
    midpoint R x y = midpoint R' x y :=
  (midpoint_eq_iff' R).2 <| (midpoint_eq_iff' R').1 rfl

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