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} [DivisionRing R] [CharZero R] [AddCommGroup V] [Module R V] [AddTorsor V P] (a b : P) : (AffineMap.lineMap a b) 2⁻¹ = midpoint R a b

theorem lineMap_one_half {R : Type u_1} {V : Type u_2} {P : Type u_3} [DivisionRing R] [CharZero R] [AddCommGroup V] [Module R V] [AddTorsor V P] (a b : P) : (AffineMap.lineMap a b) (1 / 2) = midpoint R a b

theorem homothety_invOf_two {R : Type u_1} {V : Type u_2} {P : Type u_3} [CommRing R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] (a b : P) : (AffineMap.homothety a ⅟2) b = midpoint R a b

theorem homothety_inv_two {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [CharZero k] [AddCommGroup V] [Module k V] [AddTorsor V P] (a b : P) : (AffineMap.homothety a 2⁻¹) b = midpoint k a b

theorem homothety_one_half {k : Type u_1} {V : Type u_2} {P : Type u_3} [Field k] [CharZero k] [AddCommGroup V] [Module k V] [AddTorsor V P] (a 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} [Ring k] [Invertible 2] [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] [(i : ι) → AddTorsor (V i) (P i)] (f g : (i : ι) → P i) (i : ι) : midpoint k f g i = midpoint k (f i) (g i)