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

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.

Equations
    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