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.

The divisors of a product of natural numbers are the pointwise product of the divisors of the factors.

Nat.divisors as a MonoidHom.

Equations
Instances For
    theorem Nat.Prime.divisors_sq {p : } (hp : Prime p) :
    theorem Finset.nat_divisors_prod {ι : Type u_1} (s : Finset ι) (f : ι) :