Skip to content

Commit 510dd07

Browse files
rwstYaelDillies
andauthored
Update FormalConjectures/OEIS/56777.lean
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
1 parent 1acca26 commit 510dd07

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

FormalConjectures/OEIS/56777.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@ def a (n : ℕ) : Prop :=
3838

3939
/-- A number $n$ comes from a prime quadruple $(p, p+2, p+6, p+8)$ if
4040
$n = p(p+8)$ for some prime $p$ where $p$, $p+2$, $p+6$, $p+8$ are all prime. -/
41-
def comesFromPrimeQuadruple (n : ℕ) : Prop :=
41+
def ComesFromPrimeQuadruple (n : ℕ) : Prop :=
4242
∃ p : ℕ, p.Prime ∧ (p + 2).Prime ∧ (p + 6).Prime ∧ (p + 8).Prime ∧ n = p * (p + 8)
4343

4444
/-- $65$ is in the sequence A056777. -/

0 commit comments

Comments
 (0)