Skip to content

Commit 92b003b

Browse files
committed
chore(Tactic/Positivity): import Algebra.Order.Field.Basic (#38797)
This is justified by the fact that said file contains some pretty basic positivity extensions that are hard to locate otherwise. From AddCombi
1 parent 606efcb commit 92b003b

1 file changed

Lines changed: 1 addition & 0 deletions

File tree

Mathlib/Tactic/Positivity.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
module
22

3+
public import Mathlib.Algebra.Order.Field.Basic
34
public import Mathlib.Tactic.Positivity.Basic
45
public import Mathlib.Tactic.Positivity.Finset

0 commit comments

Comments
 (0)