Nat.divisors as a multiplicative homomorpism

The main definition of this file is Nat.divisorsHom : ℕ →* Finset ℕ, exhibiting Nat.divisors as a multiplicative homomorphism from ℕ to Finset ℕ.

theorem Nat.divisors_mul (m : ℕ) (n : ℕ) : Nat.divisors (m * n) = Nat.divisors m * Nat.divisors n

The divisors of a product of natural numbers are the pointwise product of the divisors of the factors.

@[simp]

theorem Nat.divisorsHom_apply (n : ℕ) : Nat.divisorsHom n = Nat.divisors n

def Nat.divisorsHom : ℕ →* Finset ℕ

Nat.divisors as a MonoidHom.

Equations

• Nat.divisorsHom = { toOneHom := { toFun := Nat.divisors, map_one' := Nat.divisors_one }, map_mul' := Nat.divisors_mul }

theorem Nat.Prime.divisors_sq {p : ℕ} (hp : Nat.Prime p) : Nat.divisors (p ^ 2) = {p ^ 2, p, 1}

theorem List.nat_divisors_prod (l : List ℕ) : Nat.divisors (List.prod l) = List.prod (List.map Nat.divisors l)

theorem Multiset.nat_divisors_prod (s : Multiset ℕ) : Nat.divisors (Multiset.prod s) = Multiset.prod (Multiset.map Nat.divisors s)

theorem Finset.nat_divisors_prod {ι : Type u_1} (s : Finset ι) (f : ι → ℕ) : Nat.divisors (Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => Nat.divisors (f i)