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} [DivisionRing R] [CharZero R] [AddCommGroup V] [Module R V] [AddTorsor V P] (a : P) (b : P) :
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 : P) (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 : P) (b : P) :
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 : P) (b : P) :
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 : 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} [Field k] [Invertible 2] [(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)