From 78261225eb5cedc61c5c74ecb44e5b385d13b733 Mon Sep 17 00:00:00 2001
From: Moritz Doll <moritz.doll@googlemail.com>
Date: Tue, 7 Mar 2023 07:27:01 +0000
Subject: [PATCH] chore(linear_algebra/affine_space/midpoint): factor out
 lemmas about char_zero (#18555)

This removes the dependency on `char_p` in `analysis.convex.segment` and `analysis.normed.group.add_torsor`.
---
 src/analysis/convex/between.lean              |  1 +
 src/analysis/convex/slope.lean                |  1 +
 src/analysis/normed_space/add_torsor.lean     |  2 +-
 .../normed_space/affine_isometry.lean         |  1 +
 src/analysis/normed_space/mazur_ulam.lean     |  1 -
 src/linear_algebra/affine_space/midpoint.lean | 32 +-----------
 .../affine_space/midpoint_zero.lean           | 49 +++++++++++++++++++
 src/linear_algebra/affine_space/ordered.lean  |  2 +-
 8 files changed, 55 insertions(+), 34 deletions(-)
 create mode 100644 src/linear_algebra/affine_space/midpoint_zero.lean

diff --git a/src/analysis/convex/between.lean b/src/analysis/convex/between.lean
index 11d1e62efd2cc..1c1e2653347de 100644
--- a/src/analysis/convex/between.lean
+++ b/src/analysis/convex/between.lean
@@ -6,6 +6,7 @@ Authors: Joseph Myers
 import data.set.intervals.group
 import analysis.convex.segment
 import linear_algebra.affine_space.finite_dimensional
+import linear_algebra.affine_space.midpoint_zero
 import tactic.field_simp
 
 /-!
diff --git a/src/analysis/convex/slope.lean b/src/analysis/convex/slope.lean
index 103c2f74bca6f..b60a692638e25 100644
--- a/src/analysis/convex/slope.lean
+++ b/src/analysis/convex/slope.lean
@@ -5,6 +5,7 @@ Authors: Yury Kudriashov, Malo Jaffré
 -/
 import analysis.convex.function
 import tactic.field_simp
+import tactic.linarith
 
 /-!
 # Slopes of convex functions
diff --git a/src/analysis/normed_space/add_torsor.lean b/src/analysis/normed_space/add_torsor.lean
index 73d58324cfd32..72d42650c7308 100644
--- a/src/analysis/normed_space/add_torsor.lean
+++ b/src/analysis/normed_space/add_torsor.lean
@@ -5,7 +5,7 @@ Authors: Joseph Myers, Yury Kudryashov
 -/
 import analysis.normed_space.basic
 import analysis.normed.group.add_torsor
-import linear_algebra.affine_space.midpoint
+import linear_algebra.affine_space.midpoint_zero
 import linear_algebra.affine_space.affine_subspace
 import topology.instances.real_vector_space
 
diff --git a/src/analysis/normed_space/affine_isometry.lean b/src/analysis/normed_space/affine_isometry.lean
index efb9b75d83be6..0f62bc036be7c 100644
--- a/src/analysis/normed_space/affine_isometry.lean
+++ b/src/analysis/normed_space/affine_isometry.lean
@@ -7,6 +7,7 @@ import analysis.normed_space.linear_isometry
 import analysis.normed.group.add_torsor
 import analysis.normed_space.basic
 import linear_algebra.affine_space.restrict
+import linear_algebra.affine_space.midpoint_zero
 
 /-!
 # Affine isometries
diff --git a/src/analysis/normed_space/mazur_ulam.lean b/src/analysis/normed_space/mazur_ulam.lean
index 4bae238225025..ff8c8ce673de2 100644
--- a/src/analysis/normed_space/mazur_ulam.lean
+++ b/src/analysis/normed_space/mazur_ulam.lean
@@ -5,7 +5,6 @@ Authors: Yury Kudryashov
 -/
 import topology.instances.real_vector_space
 import analysis.normed_space.affine_isometry
-import linear_algebra.affine_space.midpoint
 
 /-!
 # Mazur-Ulam Theorem
diff --git a/src/linear_algebra/affine_space/midpoint.lean b/src/linear_algebra/affine_space/midpoint.lean
index 6754a232b6f86..167ffa4d2784f 100644
--- a/src/linear_algebra/affine_space/midpoint.lean
+++ b/src/linear_algebra/affine_space/midpoint.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import algebra.char_p.invertible
+import algebra.invertible
 import linear_algebra.affine_space.affine_equiv
 
 /-!
@@ -175,36 +175,6 @@ by rw midpoint_comm; simp
 
 end
 
-lemma line_map_inv_two {R : Type*} {V P : Type*} [division_ring R] [char_zero R]
-  [add_comm_group V] [module R V] [add_torsor V P] (a b : P) :
-  line_map a b (2⁻¹:R) = midpoint R a b :=
-rfl
-
-lemma line_map_one_half {R : Type*} {V P : Type*} [division_ring R] [char_zero R]
-  [add_comm_group V] [module R V] [add_torsor V P] (a b : P) :
-  line_map a b (1/2:R) = midpoint R a b :=
-by rw [one_div, line_map_inv_two]
-
-lemma homothety_inv_of_two {R : Type*} {V P : Type*} [comm_ring R] [invertible (2:R)]
-  [add_comm_group V] [module R V] [add_torsor V P] (a b : P) :
-  homothety a (⅟2:R) b = midpoint R a b :=
-rfl
-
-lemma homothety_inv_two {k : Type*} {V P : Type*} [field k] [char_zero k]
-  [add_comm_group V] [module k V] [add_torsor V P] (a b : P) :
-  homothety a (2⁻¹:k) b = midpoint k a b :=
-rfl
-
-lemma homothety_one_half {k : Type*} {V P : Type*} [field k] [char_zero k]
-  [add_comm_group V] [module k V] [add_torsor V P] (a b : P) :
-  homothety a (1/2:k) b = midpoint k a b :=
-by rw [one_div, homothety_inv_two]
-
-@[simp] lemma pi_midpoint_apply {k ι : Type*} {V : Π i : ι, Type*} {P : Π i : ι, Type*} [field k]
-  [invertible (2:k)] [Π 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) := rfl
-
 namespace add_monoid_hom
 
 variables (R R' : Type*) {E F : Type*}
diff --git a/src/linear_algebra/affine_space/midpoint_zero.lean b/src/linear_algebra/affine_space/midpoint_zero.lean
new file mode 100644
index 0000000000000..a282c780150fe
--- /dev/null
+++ b/src/linear_algebra/affine_space/midpoint_zero.lean
@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2020 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import algebra.char_p.invertible
+import linear_algebra.affine_space.midpoint
+
+/-!
+# Midpoint of a segment for characteristic zero
+
+We collect lemmas that require that the underlying ring has characteristic zero.
+
+## Tags
+
+midpoint
+-/
+
+open affine_map affine_equiv
+
+lemma line_map_inv_two {R : Type*} {V P : Type*} [division_ring R] [char_zero R]
+  [add_comm_group V] [module R V] [add_torsor V P] (a b : P) :
+  line_map a b (2⁻¹:R) = midpoint R a b :=
+rfl
+
+lemma line_map_one_half {R : Type*} {V P : Type*} [division_ring R] [char_zero R]
+  [add_comm_group V] [module R V] [add_torsor V P] (a b : P) :
+  line_map a b (1/2:R) = midpoint R a b :=
+by rw [one_div, line_map_inv_two]
+
+lemma homothety_inv_of_two {R : Type*} {V P : Type*} [comm_ring R] [invertible (2:R)]
+  [add_comm_group V] [module R V] [add_torsor V P] (a b : P) :
+  homothety a (⅟2:R) b = midpoint R a b :=
+rfl
+
+lemma homothety_inv_two {k : Type*} {V P : Type*} [field k] [char_zero k]
+  [add_comm_group V] [module k V] [add_torsor V P] (a b : P) :
+  homothety a (2⁻¹:k) b = midpoint k a b :=
+rfl
+
+lemma homothety_one_half {k : Type*} {V P : Type*} [field k] [char_zero k]
+  [add_comm_group V] [module k V] [add_torsor V P] (a b : P) :
+  homothety a (1/2:k) b = midpoint k a b :=
+by rw [one_div, homothety_inv_two]
+
+@[simp] lemma pi_midpoint_apply {k ι : Type*} {V : Π i : ι, Type*} {P : Π i : ι, Type*} [field k]
+  [invertible (2:k)] [Π 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) := rfl
diff --git a/src/linear_algebra/affine_space/ordered.lean b/src/linear_algebra/affine_space/ordered.lean
index 7b218d4cc0d05..a9ee6d0f2769a 100644
--- a/src/linear_algebra/affine_space/ordered.lean
+++ b/src/linear_algebra/affine_space/ordered.lean
@@ -5,7 +5,7 @@ Authors: Yury G. Kudryashov
 -/
 import algebra.order.invertible
 import algebra.order.module
-import linear_algebra.affine_space.midpoint
+import linear_algebra.affine_space.midpoint_zero
 import linear_algebra.affine_space.slope
 import tactic.field_simp