feat(algebra/big_operators/order): add unbundled is_absolute_value.su…

…m_le and map_prod (#10104)

Add unbundled versions of two existing lemmas.
Additionally generalize a few typeclass assumptions in an earlier file.

From the flt-regular project

src/algebra/big_operators/order.lean

@@ -511,9 +511,19 @@ begin
   exact (abv.add_le _ _).trans (add_le_add (le_refl _) ih) },
 end
 
+lemma is_absolute_value.abv_sum [semiring R] [ordered_semiring S] (abv : R → S)
+  [is_absolute_value abv] (f : ι → R) (s : finset ι) :
+  abv (∑ i in s, f i) ≤ ∑ i in s, abv (f i) :=
+(is_absolute_value.to_absolute_value abv).sum_le _ _
+
 lemma absolute_value.map_prod [comm_semiring R] [nontrivial R] [linear_ordered_comm_ring S]
   (abv : absolute_value R S) (f : ι → R) (s : finset ι) :
   abv (∏ i in s, f i) = ∏ i in s, abv (f i) :=
 abv.to_monoid_hom.map_prod f s
 
+lemma is_absolute_value.map_prod [comm_semiring R] [nontrivial R] [linear_ordered_comm_ring S]
+  (abv : R → S) [is_absolute_value abv] (f : ι → R) (s : finset ι) :
+  abv (∏ i in s, f i) = ∏ i in s, abv (f i) :=
+(is_absolute_value.to_absolute_value abv).map_prod _ _
+
 end absolute_value

src/algebra/order/absolute_value.lean

@@ -145,7 +145,7 @@ section linear_ordered_field
 
 section field
 
-variables {R S : Type*} [field R] [linear_ordered_field S] (abv : absolute_value R S)
+variables {R S : Type*} [division_ring R] [linear_ordered_field S] (abv : absolute_value R S)
 
 @[simp] protected theorem map_inv (a : R) : abv a⁻¹ = (abv a)⁻¹ :=
 abv.to_monoid_with_zero_hom.map_inv a
@@ -202,6 +202,7 @@ theorem abv_zero : abv 0 = 0 := (abv_eq_zero abv).2 rfl
 theorem abv_pos {a : R} : 0 < abv a ↔ a ≠ 0 :=
 by rw [lt_iff_le_and_ne, ne, eq_comm]; simp [abv_eq_zero abv, abv_nonneg abv]
 
+
 end ordered_semiring
 
 section linear_ordered_ring
@@ -218,9 +219,9 @@ instance abs_is_absolute_value {S} [linear_ordered_ring S] :
 
 end linear_ordered_ring
 
-section linear_ordered_field
+section linear_ordered_comm_ring
 
-variables {S : Type*} [linear_ordered_field S]
+variables {S : Type*} [linear_ordered_comm_ring S]
 
 section semiring
 variables {R : Type*} [semiring R] (abv : R → S) [is_absolute_value abv]
@@ -239,6 +240,11 @@ lemma abv_pow [nontrivial R] (abv : R → S) [is_absolute_value abv]
 
 end semiring
 
+end linear_ordered_comm_ring
+
+section linear_ordered_field
+variables {S : Type*} [linear_ordered_field S]
+
 section ring
 variables {R : Type*} [ring R] (abv : R → S) [is_absolute_value abv]
 
@@ -262,7 +268,7 @@ abs_sub_le_iff.2 ⟨sub_abv_le_abv_sub abv _ _,
 end ring
 
 section field
-variables {R : Type*} [field R] (abv : R → S) [is_absolute_value abv]
+variables {R : Type*} [division_ring R] (abv : R → S) [is_absolute_value abv]
 
 theorem abv_inv (a : R) : abv a⁻¹ = (abv a)⁻¹ :=
 (abv_hom abv).map_inv a