chore(algebra/group/pi): Split into multiple files (#5280)

This allows files that appear before `ordered_group` to still use `pi.monoid` etc.

src/algebra/group/pi.lean

@@ -4,13 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot
 -/
 import data.pi
-import algebra.ordered_group
-import algebra.group_with_zero
 import tactic.pi_instances
+import algebra.group.defs
+import algebra.group.hom
 /-!
 # Pi instances for groups and monoids
 
-This file defines instances for group, monoid, semigroup and related structures on Pi Types
+This file defines instances for group, monoid, semigroup and related structures on Pi types.
 -/
 
 universes u v w
@@ -20,19 +20,6 @@ variables (x y : Π i, f i) (i : I)
 
 namespace pi
 
-@[to_additive] instance has_one [∀ i, has_one $ f i] : has_one (Π i : I, f i) := ⟨λ _, 1⟩
-@[simp, to_additive] lemma one_apply [∀ i, has_one $ f i] : (1 : Π i, f i) i = 1 := rfl
-
-@[to_additive]
-instance has_mul [∀ i, has_mul $ f i] : has_mul (Π i : I, f i) := ⟨λ f g i, f i * g i⟩
-@[simp, to_additive] lemma mul_apply [∀ i, has_mul $ f i] : (x * y) i = x i * y i := rfl
-
-@[to_additive] instance has_inv [∀ i, has_inv $ f i] : has_inv (Π i : I, f i) := ⟨λ f i, (f i)⁻¹⟩
-@[simp, to_additive] lemma inv_apply [∀ i, has_inv $ f i] : x⁻¹ i = (x i)⁻¹ := rfl
-
-instance has_div [Π i, has_div $ f i] : has_div (Π i : I, f i) := ⟨λ f g i, f i / g i⟩
-@[simp] lemma div_apply [Π i, has_div $ f i] : (x / y) i = x i / y i := rfl
-
 @[to_additive]
 instance semigroup [∀ i, semigroup $ f i] : semigroup (Π i : I, f i) :=
 by refine_struct { mul := (*), .. }; tactic.pi_instance_derive_field
@@ -71,19 +58,6 @@ instance right_cancel_semigroup [∀ i, right_cancel_semigroup $ f i] :
   right_cancel_semigroup (Π i : I, f i) :=
 by refine_struct { mul := (*) }; tactic.pi_instance_derive_field
 
-@[to_additive]
-instance ordered_cancel_comm_monoid [∀ i, ordered_cancel_comm_monoid $ f i] :
-  ordered_cancel_comm_monoid (Π i : I, f i) :=
-by refine_struct { mul := (*), one := (1 : Π i, f i), le := (≤), lt := (<), .. pi.partial_order };
-  tactic.pi_instance_derive_field
-
-@[to_additive]
-instance ordered_comm_group [∀ i, ordered_comm_group $ f i] :
-  ordered_comm_group (Π i : I, f i) :=
-{ mul_le_mul_left := λ x y hxy c i, mul_le_mul_left' (hxy i) _,
-  ..pi.comm_group,
-  ..pi.partial_order }
-
 instance mul_zero_class [∀ i, mul_zero_class $ f i] :
   mul_zero_class (Π i : I, f i) :=
 by refine_struct { zero := (0 : Π i, f i), mul := (*), .. }; tactic.pi_instance_derive_field

src/algebra/module/ordered.lean

@@ -5,6 +5,7 @@ Authors: Frédéric Dupuis
 -/
 
 import algebra.module.pi
+import algebra.ordered_pi
 import algebra.module.prod
 import algebra.ordered_field
 

src/algebra/ordered_pi.lean

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2018 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Simon Hudon, Patrick Massot
+-/
+import algebra.group.pi
+import algebra.ordered_group
+import tactic.pi_instances
+/-!
+# Pi instances for ordered groups and monoids
+
+This file defines instances for ordered group, monoid, and related structures on Pi types.
+-/
+
+universes u v w
+variable {I : Type u}     -- The indexing type
+variable {f : I → Type v} -- The family of types already equipped with instances
+variables (x y : Π i, f i) (i : I)
+
+namespace pi
+
+@[to_additive]
+instance ordered_cancel_comm_monoid [∀ i, ordered_cancel_comm_monoid $ f i] :
+  ordered_cancel_comm_monoid (Π i : I, f i) :=
+by refine_struct { mul := (*), one := (1 : Π i, f i), le := (≤), lt := (<), .. pi.partial_order };
+  tactic.pi_instance_derive_field
+
+@[to_additive]
+instance ordered_comm_group [∀ i, ordered_comm_group $ f i] :
+  ordered_comm_group (Π i : I, f i) :=
+{ mul_le_mul_left := λ x y hxy c i, mul_le_mul_left' (hxy i) _,
+  ..pi.comm_group,
+  ..pi.partial_order }
+
+end pi

src/data/pi.lean

@@ -5,10 +5,13 @@ Authors: Simon Hudon, Patrick Massot, Eric Wieser
 -/
 import tactic.split_ifs
 import tactic.simpa
+import algebra.group.to_additive
 /-!
-# Theorems on pi types
+# Instances and theorems on pi types
 
-This file defines basic structures on Pi Types
+This file provides basic definitions and notation instances for Pi types.
+
+Instances of more sophisticated classes are defined in `pi.lean` files elsewhere.
 -/
 
 universes u v w
@@ -18,6 +21,23 @@ variables (x y : Π i, f i) (i : I)
 
 namespace pi
 
+/-! `1`, `0`, `+`, `*`, `-`, `⁻¹`, and `/` are defined pointwise. -/
+
+@[to_additive] instance has_one [∀ i, has_one $ f i] : has_one (Π i : I, f i) := ⟨λ _, 1⟩
+@[simp, to_additive] lemma one_apply [∀ i, has_one $ f i] : (1 : Π i, f i) i = 1 := rfl
+
+@[to_additive]
+instance has_mul [∀ i, has_mul $ f i] : has_mul (Π i : I, f i) := ⟨λ f g i, f i * g i⟩
+@[simp, to_additive] lemma mul_apply [∀ i, has_mul $ f i] : (x * y) i = x i * y i := rfl
+
+@[to_additive] instance has_inv [∀ i, has_inv $ f i] : has_inv (Π i : I, f i) := ⟨λ f i, (f i)⁻¹⟩
+@[simp, to_additive] lemma inv_apply [∀ i, has_inv $ f i] : x⁻¹ i = (x i)⁻¹ := rfl
+
+instance has_div [Π i, has_div $ f i] : has_div (Π i : I, f i) := ⟨λ f g i, f i / g i⟩
+@[simp] lemma div_apply [Π i, has_div $ f i] : (x / y) i = x i / y i := rfl
+
+section
+
 variables [decidable_eq I]
 variables [Π i, has_zero (f i)]
 
@@ -48,4 +68,5 @@ variables (f)
 lemma single_injective (i : I) : function.injective (single i : f i → Π i, f i) :=
 λ x y h, by simpa only [single, dif_pos] using congr_fun h i
 
+end
 end pi

src/order/pilex.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
-import algebra.group.pi
+import algebra.ordered_pi
 import order.well_founded
 import algebra.order_functions