Documentation
Goldbach
.
Basic
Search
return to top
source
Imports
Init
Goldbach.Defs
Imported by
Goldbach
.
IsGoldbachPair
.
symm
Goldbach
.
HasGoldbachDecomposition
.
four_le
Goldbach
.
hasGoldbachDecomposition_double_of_prime
Goldbach
.
hasGoldbachDecomposition_four
Goldbach
.
hasGoldbachDecomposition_six
Goldbach
.
hasGoldbachDecomposition_eight
Goldbach
.
hasGoldbachDecomposition_ten
Goldbach
.
hasGoldbachDecomposition_twelve
Goldbach
.
hasGoldbachDecomposition_fourteen
Goldbach
.
hasGoldbachDecomposition_sixteen
Goldbach
.
hasGoldbachDecomposition_eighteen
Goldbach
.
hasGoldbachDecomposition_twenty
source
theorem
Goldbach
.
IsGoldbachPair
.
symm
{
n
p
q
:
ℕ
}
(
h
:
IsGoldbachPair
n
p
q
)
:
IsGoldbachPair
n
q
p
source
theorem
Goldbach
.
HasGoldbachDecomposition
.
four_le
{
n
:
ℕ
}
(
h
:
HasGoldbachDecomposition
n
)
:
4
≤
n
source
theorem
Goldbach
.
hasGoldbachDecomposition_double_of_prime
{
p
:
ℕ
}
(
hp
:
Nat.Prime
p
)
:
HasGoldbachDecomposition
(
p
+
p
)
source
theorem
Goldbach
.
hasGoldbachDecomposition_four
:
HasGoldbachDecomposition
4
source
theorem
Goldbach
.
hasGoldbachDecomposition_six
:
HasGoldbachDecomposition
6
source
theorem
Goldbach
.
hasGoldbachDecomposition_eight
:
HasGoldbachDecomposition
8
source
theorem
Goldbach
.
hasGoldbachDecomposition_ten
:
HasGoldbachDecomposition
10
source
theorem
Goldbach
.
hasGoldbachDecomposition_twelve
:
HasGoldbachDecomposition
12
source
theorem
Goldbach
.
hasGoldbachDecomposition_fourteen
:
HasGoldbachDecomposition
14
source
theorem
Goldbach
.
hasGoldbachDecomposition_sixteen
:
HasGoldbachDecomposition
16
source
theorem
Goldbach
.
hasGoldbachDecomposition_eighteen
:
HasGoldbachDecomposition
18
source
theorem
Goldbach
.
hasGoldbachDecomposition_twenty
:
HasGoldbachDecomposition
20