Particular values of the Riemann zeta function

Reference: Wikipedia

theorem RiemannZeta.irrational_five : ∃ (x : ℝ), Irrational x ∧ riemannZeta 5 = ↑x

$\zeta(5)$ is irrational.

theorem RiemannZeta.irrational_seven : ∃ (x : ℝ), Irrational x ∧ riemannZeta 7 = ↑x

$\zeta(7)$ is irrational.

theorem RiemannZeta.irrational_nine : ∃ (x : ℝ), Irrational x ∧ riemannZeta 9 = ↑x

$\zeta(9)$ is irrational.

theorem RiemannZeta.irrational_eleven : ∃ (x : ℝ), Irrational x ∧ riemannZeta 11 = ↑x

$\zeta(11)$ is irrational.

theorem RiemannZeta.irrational_odd (n : ℕ) (hn : 0 < n) : ∃ (x : ℝ), Irrational x ∧ riemannZeta (2 * ↑n + 1) = ↑x

$\zeta(2n + 1)$ is irrational for any $n\in\mathbb{N}^{+}$.

theorem RiemannZeta.irrational_three : ∃ (x : ℝ), Irrational x ∧ riemannZeta 3 = ↑x

$\zeta(3)$ is irrational.

[Ap79] Apéry, R. (1979). Irrationalité de ζ(2) et ζ(3). Astérisque. 61: 11–13.

theorem RiemannZeta.infinite_irrational_at_odd : {n : ℕ | ∃ (x : ℝ), Irrational x ∧ riemannZeta (2 * ↑n + 1) = ↑x}.Infinite

There are infinitely many $\zeta(2n + 1)$, $n \in \mathbb{N}$, that are irrational.

[Ri00] Rivoal, T. (2000). La fonction zeta de Riemann prend une infinité de valeurs irrationnelles aux entiers impairs. Comptes Rendus de l'Académie des Sciences, Série I. 331 (4): 267–270.

theorem RiemannZeta.exists_irrational_of_five_seven_nine_eleven : ({5, 7, 9, 11} ∩ {a : ℂ | ∃ (x : ℝ), Irrational x ∧ riemannZeta a = ↑x}).Nonempty

At least one of $\zeta(5), \zeta(7), \zeta(9)$ or $\zeta(11)$ is irrational.

[Zu01] W. Zudilin (2001). One of the numbers ζ(5), ζ(7), ζ(9), ζ(11) is irrational. Russ. Math. Surv. 56 (4): 774–776.