Fungrim home page

Fungrim entry: 9fa2a1

(RH)    (for all s with sCand0Re ⁣(s)1andζ ⁣(s)=0,Re ⁣(s)=12)\left(\operatorname{RH}\right) \iff \left(\text{for all } s \text{ with } s \in \mathbb{C} \,\mathbin{\operatorname{and}}\, 0 \le \operatorname{Re}\!\left(s\right) \le 1 \,\mathbin{\operatorname{and}}\, \zeta\!\left(s\right) = 0, \,\, \operatorname{Re}\!\left(s\right) = \frac{1}{2}\right)
\left(\operatorname{RH}\right) \iff \left(\text{for all } s \text{ with } s \in \mathbb{C} \,\mathbin{\operatorname{and}}\, 0 \le \operatorname{Re}\!\left(s\right) \le 1 \,\mathbin{\operatorname{and}}\, \zeta\!\left(s\right) = 0, \,\, \operatorname{Re}\!\left(s\right) = \frac{1}{2}\right)
Fungrim symbol Notation Short description
RiemannHypothesisRH\operatorname{RH} Riemann hypothesis
CCC\mathbb{C} Complex numbers
ReRe ⁣(z)\operatorname{Re}\!\left(z\right) Real part
RiemannZetaζ ⁣(s)\zeta\!\left(s\right) Riemann zeta function
Source code for this entry:
    Formula(Equivalent(RiemannHypothesis, ForAll(s, And(Element(s, CC), LessEqual(0, Re(s), 1), Equal(RiemannZeta(s), 0)), Equal(Re(s), Div(1, 2))))))

Topics using this entry

Copyright (C) Fredrik Johansson and contributors. Fungrim is provided under the MIT license. The source code is on GitHub.

2019-09-15 11:00:55.020619 UTC