Skip to content

Commit 68ad656

Browse files
update open styling
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
1 parent 9d7ebd6 commit 68ad656

File tree

1 file changed

+1
-2
lines changed
  • FormalConjectures/ErdosProblems

1 file changed

+1
-2
lines changed

FormalConjectures/ErdosProblems/13.lean

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,7 @@ import FormalConjectures.Util.ProblemImports
2222
*Reference:* [erdosproblems.com/13](https://www.erdosproblems.com/13)
2323
-/
2424

25-
open Finset
26-
open Nat
25+
open Finset Nat
2726

2827
namespace Erdos13
2928

0 commit comments

Comments
 (0)