We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 3d07e8d commit c944dbeCopy full SHA for c944dbe
test/GCongr/inequalities.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
4
Authors: Heather Macbeth
5
-/
6
import Mathlib.Algebra.BigOperators.Order
7
+import Mathlib.Algebra.Order.Field.Basic
8
import Mathlib.Algebra.Parity
9
import Mathlib.Tactic.Linarith
10
import Mathlib.Tactic.GCongr
0 commit comments