K : Type ?u.3011502
F : Type ?u.3011505
R : Type u_1
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type u_3
Γ''₀ : Type ?u.3011520
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
v₃ : Valuation R Γ''₀
h : IsEquiv v₁ v₂
r : R
this : ↑v₁ r ≠ ↑v₁ 0 ↔ ↑v₂ r ≠ ↑v₂ 0
⊢ ↑v₁ r ≠ 0 ↔ ↑v₂ r ≠ 0
K : Type ?u.3011502
F : Type ?u.3011505
R : Type u_1
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type u_3
Γ''₀ : Type ?u.3011520
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
v₃ : Valuation R Γ''₀
h : IsEquiv v₁ v₂
r : R
⊢ ↑v₁ r ≠ 0 ↔ ↑v₂ r ≠ 0
have : v₁ r ≠ v₁ 0 ↔ v₂ r ≠ v₂ 0 := not_congr h.val_eq
no goals
K : Type ?u.3011502
F : Type ?u.3011505
R : Type u_1
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type u_3
Γ''₀ : Type ?u.3011520
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
v₃ : Valuation R Γ''₀
h : IsEquiv v₁ v₂
r : R
this : ↑v₁ r ≠ ↑v₁ 0 ↔ ↑v₂ r ≠ ↑v₂ 0
⊢ ↑v₁ r ≠ 0 ↔ ↑v₂ r ≠ 0
rwa [v₁.map_zero, v₂.map_zero] at this