fix

leanprover-community · Aug 5, 2024 · 6d707f0 · 6d707f0
1 parent 513ae5c
commit 6d707f0
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/test/algebra_rat.lean b/test/algebra_rat.lean
@@ -1,7 +1,7 @@
 import Mathlib.Algebra.Algebra.Rat
 
 /-- The two `Algebra ℚ≥0 ℚ≥0` instances should coincide. -/
-example : NNDivisionRing.toRatAlgebra = Algebra.id ℚ≥0 := rfl
+example : DivisionSemiring.toRatNNAlgebra = Algebra.id ℚ≥0 := rfl
 
 /-- The two `Algebra ℚ ℚ` instances should coincide. -/
 example : DivisionRing.toRatAlgebra = Algebra.id ℚ := rfl