R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x y : O
h : x ∣ y
z : O
hz : y = x * z
⊢ ↑v (↑(algebraMap O R) y) ≤ ↑v (↑(algebraMap O R) x)
R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x y : O
h : x ∣ y
⊢ ↑v (↑(algebraMap O R) y) ≤ ↑v (↑(algebraMap O R) x)
let ⟨z, hz⟩ := h
R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x y : O
h : x ∣ y
z : O
hz : y = x * z
⊢ ↑v (↑(algebraMap O R) x) * ↑v (↑(algebraMap O R) z) ≤ ↑v (↑(algebraMap O R) x) * 1
R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x y : O
h : x ∣ y
z : O
hz : y = x * z
⊢ ↑v (↑(algebraMap O R) y) ≤ ↑v (↑(algebraMap O R) x)
rw [← mul_one (v (algebraMap O R x)), hz, RingHom.map_mul, v.map_mul]
no goals
R : Type u
Γ₀ : Type v
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst✝³ : CommRing O
inst✝² : Algebra O R
inst✝¹ : CommRing O
inst✝ : Algebra O R
hv : Integers v O
x y : O
h : x ∣ y
z : O
hz : y = x * z
⊢ ↑v (↑(algebraMap O R) x) * ↑v (↑(algebraMap O R) z) ≤ ↑v (↑(algebraMap O R) x) * 1
exact mul_le_mul_left' (hv.2 z) _