equivProdNatFactoredNumbers_apply

Mathlib.NumberTheory.SmoothNumbers

URI: https://scilib.ai/kg/mathlib#Nat.equivProdNatFactoredNumbers_apply

← MathLib Explorer

English

Applying the equivalence to (e, m) gives p^e · m.

Русский

Применение эквивалентности к паре (e,m) даёт p^e · m.

LaTeX

$$equivProdNatFactoredNumbers hp hs (e, m) = p^e * m$$

Lean4

@[simp]
theorem equivProdNatFactoredNumbers_apply {s : Finset ℕ} {p e m : ℕ} (hp : p.Prime) (hs : p ∉ s)
    (hm : m ∈ factoredNumbers s) : equivProdNatFactoredNumbers hp hs (e, ⟨m, hm⟩) = p ^ e * m :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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