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 : O
hx : IsUnit (↑(algebraMap O R) x)
hvx : ↑v (↑(algebraMap O R) x) = 1
u : ((fun x => R) x)ˣ
hu : ↑u = ↑(algebraMap O R) x
h1 : ↑v ↑u ≤ 1
⊢ ↑v ↑u⁻¹ ≤ 1
rw [← one_mul (v _), ← hvx, ← v.map_mul, ← hu, u.mul_inv, hu, hvx, v.map_one]
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 : O
hx : IsUnit (↑(algebraMap O R) x)
hvx : ↑v (↑(algebraMap O R) x) = 1
u : ((fun x => R) x)ˣ
hu : ↑u = ↑(algebraMap O R) x
h1 : ↑v ↑u ≤ 1
h2 : ↑v ↑u⁻¹ ≤ 1
r1 : O
hr1 : ↑(algebraMap O R) r1 = ↑u
r2 : O
hr2 : ↑(algebraMap O R) r2 = ↑u⁻¹
⊢ ↑(algebraMap O R) (r1 * r2) = ↑(algebraMap O R) 1
rw [RingHom.map_mul, RingHom.map_one, hr1, hr2, Units.mul_inv]
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 : O
hx : IsUnit (↑(algebraMap O R) x)
hvx : ↑v (↑(algebraMap O R) x) = 1
u : ((fun x => R) x)ˣ
hu : ↑u = ↑(algebraMap O R) x
h1 : ↑v ↑u ≤ 1
h2 : ↑v ↑u⁻¹ ≤ 1
r1 : O
hr1 : ↑(algebraMap O R) r1 = ↑u
r2 : O
hr2 : ↑(algebraMap O R) r2 = ↑u⁻¹
⊢ ↑(algebraMap O R) (r2 * r1) = ↑(algebraMap O R) 1
rw [RingHom.map_mul, RingHom.map_one, hr1, hr2, Units.inv_mul]