We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 14b70bc commit 393dc77Copy full SHA for 393dc77
Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
@@ -32,7 +32,6 @@ namespace Rat
32
33
variable {a b c p q : ℚ}
34
35
--- FIXME: there is a panic here!
36
@[simp] lemma mkRat_nonneg {a : ℤ} (ha : 0 ≤ a) (b : ℕ) : 0 ≤ mkRat a b := by
37
simpa using divInt_nonneg ha (Int.natCast_nonneg _)
38
0 commit comments