Skip to content

Commit 56041e8

Browse files
committed
Fix typo in integer statement
1 parent 8261296 commit 56041e8

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

APAP/Integer.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,4 +8,4 @@ open Finset Real
88
public section
99

1010
theorem int {A : Finset ℕ} {N : ℕ} (hAN : A ⊆ range N) (hA : ThreeAPFree (α := ℕ) A) :
11-
∃ c > 0, #A ≤ N / exp (- c * log N ^ (12⁻¹ : ℝ)) := sorry
11+
∃ c > 0, #A ≤ N / exp (c * log N ^ (12⁻¹ : ℝ)) := sorry

0 commit comments

Comments
 (0)