[Merged by Bors] - feat(ring_theory/valuation): definition and basic properties of valuations

src/algebra/linear_ordered_comm_group_with_zero.lean

@@ -6,6 +6,7 @@ Authors: Kenny Lau, Johan Commelin, Patrick Massot
 
 import algebra.ordered_group
 import algebra.group_with_zero
+import algebra.group_with_zero_power
 
 /-!
 # Linearly ordered commutative groups with a zero element adjoined
@@ -41,6 +42,44 @@ instance linear_ordered_comm_group_with_zero.to_ordered_comm_monoid : ordered_co
     exact linear_ordered_comm_group_with_zero.mul_le_mul_left h a }
   .. ‹linear_ordered_comm_group_with_zero α› }
 
+
+section linear_ordered_comm_monoid
+/-
+The following facts are true more generally in a (linearly) ordered commutative monoid.
+-/
+
+lemma one_le_pow_of_one_le' {n : ℕ} (H : 1 ≤ x) : 1 ≤ x^n :=
+begin
+  induction n with n ih,
+  { exact le_refl 1 },
+  { exact one_le_mul_of_one_le_of_one_le H ih }
+end
+
+lemma pow_le_one_of_le_one {n : ℕ} (H : x ≤ 1) : x^n ≤ 1 :=
+begin
+  induction n with n ih,
+  { exact le_refl 1 },
+  { exact mul_le_one_of_le_one_of_le_one H ih }
+end
+
+lemma eq_one_of_pow_eq_one {n : ℕ} (hn : n ≠ 0) (H : x ^ n = 1) : x = 1 :=
+begin
+  rcases nat.exists_eq_succ_of_ne_zero hn with ⟨n, rfl⟩, clear hn,
+  induction n with n ih,
+  { simpa using H },
+  { cases le_total x 1,
+    all_goals
+    { have h1 := mul_le_mul_right' h,
+      rw pow_succ at H,
+      rw [H, one_mul] at h1 },
+    { have h2 := pow_le_one_of_le_one h,
+      exact ih (le_antisymm h2 h1) },
+    { have h2 := one_le_pow_of_one_le' h,
+      exact ih (le_antisymm h1 h2) } }
+end
+
+end linear_ordered_comm_monoid
+
 lemma zero_le_one' : (0 : α) ≤ 1 :=
 linear_ordered_comm_group_with_zero.zero_le_one
 

src/algebra/ordered_group.lean

@@ -175,6 +175,18 @@ iff.intro
    and.intro ‹a = 1› ‹b = 1›)
   (assume ⟨ha', hb'⟩, by rw [ha', hb', mul_one])
 
+@[to_additive]
+lemma one_le_mul_of_one_le_of_one_le (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ a * b :=
+have h1 : a * 1 ≤ a * b, from mul_le_mul_left' hb,
+have h2 : a ≤ a * b, by rwa mul_one a at h1,
+le_trans ha h2
+
+@[to_additive]
+lemma mul_le_one_of_le_one_of_le_one (ha : a ≤ 1) (hb : b ≤ 1) : a * b ≤ 1 :=
+have h1 : a * b ≤ a * 1, from mul_le_mul_left' hb,
+have h2 : a * b ≤ a, by rwa mul_one a at h1,
+le_trans h2 ha
+
 section mono
 
 variables {β : Type*} [preorder β] {f g : β → α}