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) :
⇑(affine_map.line_map a b) 2⁻¹ = midpoint R a b
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) :
⇑(affine_map.line_map a b) (1 / 2) = midpoint R a b
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) :
⇑(affine_map.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]
[char_zero k]
[add_comm_group V]
[module k V]
[add_torsor V P]
(a b : P) :
⇑(affine_map.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]
[char_zero k]
[add_comm_group V]
[module k V]
[add_torsor V P]
(a b : P) :
⇑(affine_map.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 : ι), add_comm_group (V i)]
[Π (i : ι), module k (V i)]
[Π (i : ι), add_torsor (V i) (P i)]
(f g : Π (i : ι), P i)
(i : ι) :