---

Step * of Lemma two-factorizations-no-repeats

∀[n:ℕ]. no_repeats(ℤ × ℤ;two-factorizations(n))
BY
{ (Auto THEN RepUR ``two-factorizations mapfilter`` 0) }

1
1. n : ℕ
⊢ no_repeats(ℤ × ℤ;map(λa.<a, n ÷ a>;filter(λa.(n rem a =z 0);[1, n + 1))))

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  no\_repeats(\mBbbZ{}  \mtimes{}  \mBbbZ{};two-factorizations(n))


By

---

Latex:
(Auto  THEN  RepUR  ``two-factorizations  mapfilter``  0)

---

Home Index