prodNatEquiv_apply — Mathlib

English

For a prime p and natural k, the forward map sends (p,k) to the prime power p^(k+1).

Русский

Для простого p и натурального k отображение вперед отправляет (p,k) в простую степень p^(k+1).

LaTeX

$$$\text{prodNatEquiv}(p,k) = \langle p^{k+1}, p, k+1, \text{prime}(p), \text{pos}(k+1), rfl\rangle$$$

Lean4

@[simp]
theorem prodNatEquiv_apply (p : Nat.Primes) (k : ℕ) :
    prodNatEquiv (p, k) = ⟨p ^ (k + 1), p, k + 1, prime_iff.mp p.prop, k.add_one_pos, rfl⟩ := by rfl

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