F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : Integers v O
x y : O
h : ↑v (↑(algebraMap O F) x) ≤ ↑v (↑(algebraMap O F) y)
hy : ↑(algebraMap O F) y ≠ 0
⊢ ↑v (↑(algebraMap O F) y)⁻¹ * ↑v (↑(algebraMap O F) x) ≤ ↑v (↑(algebraMap O F) y)⁻¹ * ↑v (↑(algebraMap O F) y)
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : Integers v O
x y : O
h : ↑v (↑(algebraMap O F) x) ≤ ↑v (↑(algebraMap O F) y)
hy : ↑(algebraMap O F) y ≠ 0
⊢ ↑v ((↑(algebraMap O F) y)⁻¹ * ↑(algebraMap O F) x) ≤ 1
rw [← v.map_one, ← inv_mul_cancel hy, v.map_mul, v.map_mul]
no goals
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : Integers v O
x y : O
h : ↑v (↑(algebraMap O F) x) ≤ ↑v (↑(algebraMap O F) y)
hy : ↑(algebraMap O F) y ≠ 0
⊢ ↑v (↑(algebraMap O F) y)⁻¹ * ↑v (↑(algebraMap O F) x) ≤ ↑v (↑(algebraMap O F) y)⁻¹ * ↑v (↑(algebraMap O F) y)
exact mul_le_mul_left' h _