feat(RingTheory/Valuation): add IsTrivialOn_lemmas (leanprover-community#35503)

Co-authored by : @xgenereux

Co-authored-by: mariainesdff <mariaines.dff@gmail.com>

Author: mariainesdff

Mathlib/RingTheory/Valuation/Basic.lean

@@ -651,6 +651,14 @@ lemma one_lt_iff_one_lt (h : v₁.IsEquiv v₂) {x : R} :
     1 < v₁ x ↔ 1 < v₂ x := by
   rw [← v₁.map_one, h.lt_iff_lt, map_one]
 
+theorem isTrivialOn {A : Type*} [CommSemiring A] [Algebra A R] (h : v₁.IsEquiv v₂)
+    (h₁ : IsTrivialOn A v₁) : IsTrivialOn A v₂ where
+  eq_one _ ha := h.eq_one_iff_eq_one.mp (IsTrivialOn.eq_one _ ha)
+
+theorem isTrivialOn_iff {A : Type*} [CommSemiring A] [Algebra A R] (h : v₁.IsEquiv v₂) :
+    IsTrivialOn A v₁ ↔ IsTrivialOn A v₂ :=
+  ⟨fun h₁ ↦ h.isTrivialOn h₁, fun h₂ ↦ h.symm.isTrivialOn h₂⟩
+
 end IsEquiv
 
 section LinearOrderedCommMonoidWithZero

Mathlib/RingTheory/Valuation/Integers.lean

@@ -109,6 +109,10 @@ lemma nontrivial_iff (hv : v.Integers O) : Nontrivial O ↔ Nontrivial R := by
 
 end Integers
 
+theorem IsTrivialOn.of_le_one {k : Type*} [Field k] [Algebra k R] (v : Valuation R Γ₀)
+    (hle : ∀ (x : k), v (algebraMap k R x) ≤ 1) : v.IsTrivialOn k where
+  eq_one a ha := Valuation.Integers.one_of_isUnit' (IsUnit.mk0 a ha) hle
+
 lemma integers_nontrivial (v : Valuation R Γ₀) :
     Nontrivial v.integer ↔ Nontrivial R :=
   (Valuation.integer.integers v).nontrivial_iff