chore(linear_algebra/affine_space/midpoint): factor out lemmas about char_zero (#18555)

mcdoll · mcdoll · commit 78261225eb5c · 2023-03-07T07:27:01.000Z
This removes the dependency on `char_p` in `analysis.convex.segment` and `analysis.normed.group.add_torsor`.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
 
