Divisor Simprocs

This file implements (d)simprocs to compute various objects related to divisors:

• Nat.divisors_ofNat: computes Nat.divisors n for explicit values of n
• Nat.properDivisors_ofNat: computes Nat.properDivisors n for explicit values of n

def Nat.divisors_ofNat : Lean.Meta.Simp.DSimproc

The dsimproc Nat.divisors_ofNat computes the finset Nat.divisors n when n is a numeral. For instance, this simplifies Nat.divisors 6 to {1, 2, 3, 6}.

Equations

• One or more equations did not get rendered due to their size.

def Nat.properDivisors_ofNat : Lean.Meta.Simp.DSimproc

The dsimproc Nat.properDivisors_ofNat computes the finset Nat.properDivisors n when n is a numeral. For instance, this simplifies Nat.properDivisors 12 to {1, 2, 3, 4, 6}.

Equations

• One or more equations did not get rendered due to their size.