# Documentation

Mathlib.LinearAlgebra.AffineSpace.MidpointZero

# Midpoint of a segment for characteristic zero #

We collect lemmas that require that the underlying ring has characteristic zero.

## Tags #

midpoint

theorem lineMap_inv_two {R : Type u_1} {V : Type u_2} {P : Type u_3} [] [] [] [Module R V] [] (a : P) (b : P) :
↑() 2⁻¹ = midpoint R a b
theorem lineMap_one_half {R : Type u_1} {V : Type u_2} {P : Type u_3} [] [] [] [Module R V] [] (a : P) (b : P) :
↑() (1 / 2) = midpoint R a b
theorem homothety_invOf_two {R : Type u_1} {V : Type u_2} {P : Type u_3} [] [] [] [Module R V] [] (a : P) (b : P) :
↑() b = midpoint R a b
theorem homothety_inv_two {k : Type u_1} {V : Type u_2} {P : Type u_3} [] [] [] [Module k V] [] (a : P) (b : P) :
↑() b = midpoint k a b
theorem homothety_one_half {k : Type u_1} {V : Type u_2} {P : Type u_3} [] [] [] [Module k V] [] (a : P) (b : P) :
↑(AffineMap.homothety a (1 / 2)) b = midpoint k a b
@[simp]
theorem pi_midpoint_apply {k : Type u_1} {ι : Type u_2} {V : ιType u_3} {P : ιType u_4} [] [] [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] [(i : ι) → AddTorsor (V i) (P i)] (f : (i : ι) → P i) (g : (i : ι) → P i) (i : ι) :
midpoint k ((i : ι) → V i) ((i : ι) → P i) DivisionRing.toRing inst✝ Pi.addCommGroup (Pi.module ι (fun i => V i) k) Pi.instAddTorsor f g i = midpoint k (f i) (g i)