# 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`

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

Instances For

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

Instances For