Documentation
LeanPool
.
Zeta32
.
Results
Search
return to top
source
Imports
Init
LeanPool.Zeta32.Final
Imported by
Zeta32Acceptance
.
one_zeta_two_zeta_three_linearIndependent
Zeta32Acceptance
.
one_zeta_two_zeta_three_linearIndependent_series
Zeta32 — Results.
source
theorem
Zeta32Acceptance
.
one_zeta_two_zeta_three_linearIndependent
:
LinearIndependent
ℚ
![
1
,
riemannZeta
2
,
riemannZeta
3
]
source
theorem
Zeta32Acceptance
.
one_zeta_two_zeta_three_linearIndependent_series
(
a
b
c
:
ℚ
)
(
h
:
↑
a
+
↑
b
*
∑'
(
k
:
ℕ
)
,
1
/
(
↑
k
+
1
)
^
2
+
↑
c
*
∑'
(
k
:
ℕ
)
,
1
/
(
↑
k
+
1
)
^
3
=
0
)
:
a
=
0
∧
b
=
0
∧
c
=
0