exp_one_near_20 — Mathlib

English

There exists a rational r = 363916618873/133877442384 with |exp(1) - r| ≤ 10^-20.

Русский

Существует рациональное число r = 363916618873/133877442384 такое, что |exp(1) - r| ≤ 10^-20.

LaTeX

$$$|\exp(1) - \frac{363916618873}{133877442384}| \le 10^{-20}$$$

Lean4

theorem exp_one_near_20 : |exp 1 - 363916618873 / 133877442384| ≤ 1 / 10 ^ 20 :=
  by
  apply exp_approx_start
  iterate 21 refine exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) ?_
  refine exp_approx_end' _ (by norm_num1; rfl) _ (by norm_cast) (by simp) ?_
  norm_num1

Похожие утверждения