Divisor Simprocs

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

• Nat.divisorsEq: computes Nat.divisors n for explicit values of n
• Nat.properDivisorsEq: computes Nat.properDivisors n for explicit values of n

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

The Nat.divisorsEq computes the finset Nat.divisors n when n is a natural number literal. 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

Compute the finset Nat.properDivisorsEq n when n is a numeral. For instance, this simplifies Nat.properDivisorsEq 12 to {1, 2, 3, 4, 6}.

Equations

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