English
Let divisors(n) denote the finite set of positive divisors of n. Then divisors(1) = {1} and divisors(ab) = divisors(a) · divisors(b) for all a,b ∈ ℕ, where the product of Finsets is the Finset of all pairwise products. In particular, divisors is a monoid hom from (ℕ, ×) to (Finset ℕ, ×).
Русский
Пусть divisors(n) обозначает конечное множество делителей числа n. Тогда divisors(1) = {1} и divisors(ab) = divisors(a) · divisors(b) для всех a,b ∈ ℕ, где произведение двух множеств определяется как множество всех произведений элементов. Следовательно, divisors является моноид-гомоморфизмом от (ℕ, ×) к (Finset ℕ, ×).
LaTeX
$$$\\operatorname{divisors}(1)=\\{1\\},\\quad \\operatorname{divisors}(ab)=\\operatorname{divisors}(a)\\cdot\\operatorname{divisors}(b)\\quad (a,b\\in\\mathbb{N}),$ i.e. divisors is a monoid hom from $(\\mathbb{N},\\cdot)$ to $(\\mathrm{Finset}(\\mathbb{N}),\\cdot)$.$$
Lean4
/-- `Nat.divisors` as a `MonoidHom`. -/
@[simps]
def divisorsHom : ℕ →* Finset ℕ where
toFun := Nat.divisors
map_mul' := divisors_mul
map_one' := divisors_one
