coe_nat_two_pow_pred — Mathlib

English

For all natural p, the integer obtained by casting (2^p − 1) from natural to integers equals the usual integer value of 2^p − 1.

Русский

Для любого натурального p целое число, полученное путем приведения (2^p − 1) из натуральных чисел к целым, равно обычному целому значению 2^p − 1.

LaTeX

$$((2^p - 1 : ℕ) : ℤ) = (2^p - 1 : ℤ)$$

Lean4

theorem coe_nat_two_pow_pred (p : ℕ) : ((2 ^ p - 1 : ℕ) : ℤ) = (2 ^ p - 1 : ℤ) :=
  Int.natCast_pow_pred 2 p (by decide)

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