chore(ring_theory/valuation/basic): fix valuation_apply (#13045)

Follow-up to #12914.
leanprover-community · Mar 29, 2022 · 119eb05 · 119eb05
1 parent e4c6449
commit 119eb05
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/ring_theory/valuation/basic.lean b/src/ring_theory/valuation/basic.lean
@@ -496,7 +496,8 @@ theorem of_apply : (of f h0 h1 hadd hmul) r = f r := rfl
 `add_valuation.of`). -/
 def valuation : valuation R (multiplicative (order_dual Γ₀)) := v
 
-@[simp] lemma valuation_apply (r : R) : v.valuation r = multiplicative.of_add (v r) := rfl
+@[simp] lemma valuation_apply (r : R) :
+  v.valuation r = multiplicative.of_add (order_dual.to_dual (v r)) := rfl
 
 end