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 : ℕ) : (m * n).divisors = m.divisors * n.divisors

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 = n.divisors

def Nat.divisorsHom : ℕ →* Finset ℕ

Nat.divisors as a MonoidHom.

Equations

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

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

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

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

theorem Finset.nat_divisors_prod {ι : Type u_1} (s : Finset ι) (f : ι → ℕ) : (∏ i ∈ s, f i).divisors = ∏ i ∈ s, (f i).divisors