English
Let p be a prime not contained in a finite set s of natural numbers, and consider the canonical bijection that identifies a pair (a, t) with a factor p^a multiplied by t (where t corresponds to an element of the factorization over s). Then the bijection maps (a, t) to p^a · t for every a ∈ ℕ and t ∈ factoredNumbers s.
Русский
Пусть p — простое число, не принадлежащее конечному множеству s пополов натуральных чисел, и пусть существует каноническая биекция, которая отправляет пару (a, t) в факторизацию p^a·t (где t ∈ factoredNumbers s). Тогда образ этой пары равен p^a · t.
LaTeX
$$$\\mathrm{equivProdNatFactoredNumbers}(hp, hs)(a, t) = p^{a} \\cdot t$$$
Lean4
@[simp]
theorem equivProdNatFactoredNumbers_apply' {s : Finset ℕ} {p : ℕ} (hp : p.Prime) (hs : p ∉ s)
(x : ℕ × factoredNumbers s) : equivProdNatFactoredNumbers hp hs x = p ^ x.1 * x.2 :=
rfl
