Documentation

Mathlib.Data.Finset.NatDivisors

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

Nat.divisors as a MonoidHom.

Equations
Instances For
    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 Finset.nat_divisors_prod {ι : Type u_1} (s : Finset ι) (f : ι) :
    (∏ is, f i).divisors = is, (f i).divisors