mathlib3 documentation

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} [division_ring R] [char_zero R] [add_comm_group V] [module R V] [add_torsor V P] (a b : P) :
theorem line_map_one_half {R : Type u_1} {V : Type u_2} {P : Type u_3} [division_ring R] [char_zero R] [add_comm_group V] [module R V] [add_torsor V P] (a b : P) :
theorem homothety_inv_of_two {R : Type u_1} {V : Type u_2} {P : Type u_3} [comm_ring R] [invertible 2] [add_comm_group V] [module R V] [add_torsor V P] (a b : P) :
theorem homothety_inv_two {k : Type u_1} {V : Type u_2} {P : Type u_3} [field k] [char_zero k] [add_comm_group V] [module k V] [add_torsor V P] (a b : P) :
theorem homothety_one_half {k : Type u_1} {V : Type u_2} {P : Type u_3} [field k] [char_zero k] [add_comm_group V] [module k V] [add_torsor V P] (a b : P) :
@[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 : ι), module k (V i)] [Π (i : ι), add_torsor (V i) (P i)] (f g : Π (i : ι), P i) (i : ι) :
midpoint k f g i = midpoint k (f i) (g i)