Nicol numbers

DefinitionNicol numbers#✓fully proved

A Nicol number is a positive integer \(n\) that divides \(\varphi(n) + \sigma(n)\), where \(\varphi\) is Euler's totient function and \(\sigma(n)\) is the sum of the positive divisors of \(n\).

def IsNicolNumber (n : ℕ) : Prop :=
  0 < n ∧ n ∣ Nat.totient n + ∑ d ∈ n.divisors, d

Sources

• JIS VOL14/Tang, https://cs.uwaterloo.ca/journals/JIS/VOL14/Tang2/tang72.tex, lines 77–90.

Used by 1

Used byEvery \(t\)-Nicol number is a Nicol number

Definition\(t\)-Nicol numbers#✓fully proved

For a natural number \(t\), a \(t\)-Nicol number is a positive integer \(n\) such that \(\varphi(n) + \sigma(n) = t n\), where \(\varphi\) is Euler's totient function and \(\sigma(n)\) is the sum of the positive divisors of \(n\).

def IsTNicolNumber (t n : ℕ) : Prop :=
  0 < n ∧ Nat.totient n + ∑ d ∈ n.divisors, d = t * n

Used by 1

Used byEvery \(t\)-Nicol number is a Nicol number

TheoremEvery \(t\)-Nicol number is a Nicol number#✓fully proved

For all natural numbers \(t\) and \(n\), if \(n\) is a \(t\)-Nicol number, then \(n\) is a Nicol number.

theorem IsTNicolNumber.isNicolNumber {t n : ℕ} (h : IsTNicolNumber t n) :
    IsNicolNumber n

Uses 2

Statement usesNicol numbers · \(t\)-Nicol numbers

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.