# mathlib3documentation

linear_algebra.affine_space.midpoint_zero

# Midpoint of a segment for characteristic zero #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Tags #

midpoint

theorem line_map_inv_two {R : Type u_1} {V : Type u_2} {P : Type u_3} [char_zero R] [ V] [ P] (a b : P) :
b) 2⁻¹ = a b
theorem line_map_one_half {R : Type u_1} {V : Type u_2} {P : Type u_3} [char_zero R] [ V] [ P] (a b : P) :
b) (1 / 2) = a b
theorem homothety_inv_of_two {R : Type u_1} {V : Type u_2} {P : Type u_3} [comm_ring R] [invertible 2] [ V] [ P] (a b : P) :
( 2)) b = a b
theorem homothety_inv_two {k : Type u_1} {V : Type u_2} {P : Type u_3} [field k] [char_zero k] [ V] [ P] (a b : P) :
b = a b
theorem homothety_one_half {k : Type u_1} {V : Type u_2} {P : Type u_3} [field k] [char_zero k] [ V] [ P] (a b : P) :
(1 / 2)) b = a b
@[simp]
theorem pi_midpoint_apply {k : Type u_1} {ι : Type u_2} {V : ι Type u_3} {P : ι Type u_4} [field k] [invertible 2] [Π (i : ι), add_comm_group (V i)] [Π (i : ι), (V i)] [Π (i : ι), add_torsor (V i) (P i)] (f g : Π (i : ι), P i) (i : ι) :
f g i = (f i) (g i)