equivProdNatSmoothNumbers_apply — Mathlib

English

Let p be a prime and m ∈ p.smoothNumbers. Then the image of (e, ⟨m, hm⟩) under the natural product-decomposition bijection is p^e · m; equivalently, the e-th p-part separated from m via the bijection yields p^e m.

Русский

Пусть p — простое и m ∈ p.smoothNumbers. Тогда образ пары (e, ⟨m, hm⟩) под естественной биекции разложения на произведение равен p^e · m.

LaTeX

$$$\mathrm{equivProdNatSmoothNumbers}(p, (e, \langle m, hm \rangle)) = p^{e} \cdot m$$$

Lean4

@[simp]
theorem equivProdNatSmoothNumbers_apply {p e m : ℕ} (hp : p.Prime) (hm : m ∈ p.smoothNumbers) :
    equivProdNatSmoothNumbers hp (e, ⟨m, hm⟩) = p ^ e * m :=
  rfl

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