Documentation

Mathlib.Data.Finset.NatDivisors

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 ℕ.

source
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.

source
def Nat.divisorsHom :
ℕ →* Finset ℕ

Nat.divisors as a MonoidHom.

Instances For
    source
    @[simp]
    theorem Nat.divisorsHom_apply (n : ℕ) :
    divisorsHom n = n.divisors
    source
    theorem Nat.Prime.divisors_sq {p : ℕ} (hp : Prime p) :
    (p ^ 2).divisors = {p ^ 2, p, 1}
    source
    theorem List.nat_divisors_prod (l : List ℕ) :
    l.prod.divisors = (map Nat.divisors l).prod
    source
    theorem Multiset.nat_divisors_prod (s : Multiset ℕ) :
    s.prod.divisors = (map Nat.divisors s).prod
    source
    theorem Finset.nat_divisors_prod {ι : Type u_1} (s : Finset ι) (f : ι → ℕ) :
    (∏ i ∈ s, f i).divisors = ∏ i ∈ s, (f i).divisors