feat(ring_theory/valuation): definition and basic properties of valua…

…tions (#3222)

From the perfectoid project.

docs/references.bib

@@ -266,4 +266,11 @@ @Article{ghys87:groupes
   pages =	 {81-106},
   doi =		 {10.1090/conm/058.3/893858},
   language =	 {french}
-}
+}
+
+@misc{wedhorn_adic,
+Author = {Torsten Wedhorn},
+Title = {Adic Spaces},
+Year = {2019},
+Eprint = {arXiv:1910.05934},
+}

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,65 @@ 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
+
+lemma pow_eq_one_iff {n : ℕ} (hn : n ≠ 0) : x ^ n = 1 ↔ x = 1 :=
+⟨eq_one_of_pow_eq_one hn, by { rintro rfl, exact one_pow _ }⟩
+
+lemma one_le_pow_iff {n : ℕ} (hn : n ≠ 0) : 1 ≤ x^n ↔ 1 ≤ x :=
+begin
+  refine ⟨_, one_le_pow_of_one_le'⟩,
+  contrapose!,
+  intro h, apply lt_of_le_of_ne (pow_le_one_of_le_one (le_of_lt h)),
+  rw [ne.def, pow_eq_one_iff hn],
+  exact ne_of_lt h,
+end
+
+lemma pow_le_one_iff {n : ℕ} (hn : n ≠ 0) : x^n ≤ 1 ↔ x ≤ 1 :=
+begin
+  refine ⟨_, pow_le_one_of_le_one⟩,
+  contrapose!,
+  intro h, apply lt_of_le_of_ne (one_le_pow_of_one_le' (le_of_lt h)),
+  rw [ne.def, eq_comm, pow_eq_one_iff hn],
+  exact ne_of_gt h,
+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 : β → α}