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}
[Field k]
[Invertible 2]
[(i : ι) → AddCommGroup (V i)]
[(i : ι) → Module k (V i)]
[(i : ι) → AddTorsor (V i) (P i)]
(f g : (i : ι) → P i)
(i : ι)
: