equivProdNatSmoothNumbers_apply' — Mathlib

English

Let hp be a prime and x = (e, m) with m ∈ p.smoothNumbers. Then equivProdNatSmoothNumbers hp x = p^e · m.

Русский

Пусть hp — простое, и x = (e, m) с m ∈ p.smoothNumbers. Тогда equivProdNatSmoothNumbers hp x = p^e · m.

LaTeX

$$$\mathrm{equivProdNatSmoothNumbers}(hp, x) = p^{x.1} \cdot x.2,$ where $x = (x.1, x.2)$ and $x.2 \in p.smoothNumbers$$$

Lean4

@[simp]
theorem equivProdNatSmoothNumbers_apply' {p : ℕ} (hp : p.Prime) (x : ℕ × p.smoothNumbers) :
    equivProdNatSmoothNumbers hp x = p ^ x.1 * x.2 :=
  rfl

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