11import Mathlib.Algebra.Order.AbsoluteValue.Basic
2- import Mathlib.Tactic
2+ import Mathlib.Tactic.Linarith
33
44namespace AbsoluteValue
55
6- variable {F S : Type *} [Field F] [LinearOrderedField S] {v w : AbsoluteValue F S}
6+ variable {F S : Type *} [Field F] [Field S] [LinearOrder S]
7+ {v w : AbsoluteValue F S}
78
8- theorem inv_pos {x : F} (h : 0 < v x) : 0 < v x⁻¹ := by
9+ theorem inv_pos [IsStrictOrderedRing S] {x : F} (h : 0 < v x) : 0 < v x⁻¹ := by
910 rwa [IsAbsoluteValue.abv_inv v, _root_.inv_pos]
1011
11- theorem ne_zero_of_lt_one {F S : Type *} [Field F] [LinearOrderedField S]
12+ theorem ne_zero_of_lt_one {F S : Type *} [Field F] [Field S] [LinearOrder S] [IsStrictOrderedRing S]
1213 {v : AbsoluteValue F S} {x : F} (hv : 1 < v x) : x ≠ 0 :=
1314 fun hx => by linarith [map_zero v ▸ hx ▸ hv]
1415
15- theorem isNontrivial_iff_exists_abv_gt_one {F S : Type *} [Field F] [LinearOrderedField S]
16- {v : AbsoluteValue F S} :
16+ theorem isNontrivial_iff_exists_abv_gt_one {F S : Type *} [Field F] [Field S] [LinearOrder S]
17+ [IsStrictOrderedRing S] {v : AbsoluteValue F S} :
1718 v.IsNontrivial ↔ ∃ x, 1 < v x := by
1819 refine ⟨fun h => h.exists_abv_gt_one, fun ⟨x, hx⟩ => ?_⟩
1920 refine ⟨x⁻¹, ?_, ?_⟩
@@ -23,10 +24,12 @@ theorem isNontrivial_iff_exists_abv_gt_one {F S : Type*} [Field F] [LinearOrdere
2324theorem nonpos_iff (x : F) : v x ≤ 0 ↔ v x = 0 := by
2425 simp only [le_antisymm_iff, v.nonneg _, and_true]
2526
27+ variable [IsStrictOrderedRing S]
2628theorem inv_lt_one_iff {x : F} : v x⁻¹ < 1 ↔ x = 0 ∨ 1 < v x := by
2729 simp only [map_inv₀, inv_lt_one_iff₀, nonpos_iff, map_eq_zero]
2830
29- theorem mul_one_div_lt_iff {y : F} (x : F) (h : 0 < v y) : v (x * (1 / y)) < 1 ↔ v x < v y := by
31+ theorem mul_one_div_lt_iff {y : F} (x : F) (h : 0 < v y) :
32+ v (x * (1 / y)) < 1 ↔ v x < v y := by
3033 rw [map_mul, one_div, map_inv₀, mul_inv_lt_iff₀ h, one_mul]
3134
3235theorem mul_one_div_pow_lt_iff {n : ℕ} {y : F} (x : F) (h : 0 < v y) :
@@ -51,17 +54,18 @@ theorem eq_one_iff_of_lt_one_iff (h : ∀ x, v x < 1 ↔ w x < 1) (x : F) : v x
5154
5255variable (w)
5356
57+ omit [IsStrictOrderedRing S] in
5458theorem pos_of_pos {a : F} (hv : 0 < v a) : 0 < w a := by
5559 rwa [AbsoluteValue.pos_iff] at hv ⊢
5660
57- variable {R S : Type *} [OrderedRing S] [Semiring R] (v : AbsoluteValue R S) [IsDomain S ]
58- [Nontrivial R]
61+ variable {R S : Type *} [Ring S] [PartialOrder S] [Semiring R ]
62+ (v : AbsoluteValue R S) [IsDomain S] [Nontrivial R]
5963
6064theorem one_add_pow_le (a : R) (n : ℕ) : v (1 + a ^ n) ≤ 1 + v a ^ n :=
6165 le_trans (v.add_le _ _) (by rw [map_one, map_pow])
6266
63- variable {R S : Type *} [OrderedCommRing S] [Ring R] (v : AbsoluteValue R S) [NoZeroDivisors S ]
64- [IsDomain S] [Nontrivial R]
67+ variable {R S : Type *} [CommRing S] [PartialOrder S] [IsOrderedRing S] [Ring R ]
68+ (v : AbsoluteValue R S) [NoZeroDivisors S] [IsDomain S] [Nontrivial R]
6569
6670theorem one_sub_pow_le (a : R) (n : ℕ) : 1 - v a ^ n ≤ v (1 + a ^ n) :=
6771 le_trans (by rw [map_one, map_pow]) (v.le_add 1 (a ^ n))
0 commit comments