Nat.divisors as a multiplicative homomorphism

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.

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 }

@[simp]

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

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

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

theorem Multiset.nat_divisors_prod (s : Multiset ℕ) : s.prod.divisors = (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

theorem Nat.Coprime.mul_injOn_divisors {m n : ℕ} (hmn : m.Coprime n) : Set.InjOn (fun (p : ℕ × ℕ) => p.1 * p.2) ↑(m.divisors ×ˢ n.divisors)

Products of divisors taken from coprime naturals are unique.

theorem Nat.Coprime.divisors_mul {m n : ℕ} (hmn : m.Coprime n) : (m * n).divisors = Finset.map { toFun := fun (p : { x : ℕ × ℕ // x ∈ ↑(m.divisors ×ˢ n.divisors) }) => (↑p).1 * (↑p).2, inj' := ⋯ } (m.divisors ×ˢ n.divisors).attach

A variant of Nat.divisors_mul with a more structured RHS.