# 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 f g i = midpoint k (f i) (g i)