coe_prodNatEquiv_apply

Mathlib.Data.Nat.Factorization.PrimePow

URI: https://scilib.ai/kg/mathlib#Nat.Primes.coe_prodNatEquiv_apply

English

The underlying natural number of the forward image is p^(k+1).

Русский

Число, соответствующее образу в естественных числах, равно p^(k+1).

LaTeX

$$$\bigl(prodNatEquiv(p,k)\bigr) = p^{k+1}$$$

Lean4

@[simp]
theorem coe_prodNatEquiv_apply (p : Nat.Primes) (k : ℕ) : (prodNatEquiv (p, k) : ℕ) = p ^ (k + 1) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru