Unitary divisors

3 fully proved

Unitary divisors

DefinitionUnitary divisors#✓fully proved

For a natural number \(n\), the unitary divisors of \(n\) are the divisors \(d\) of \(n\) that are coprime to the complementary divisor \(n/d\), that is, with \(\gcd(d, n/d) = 1\). For \(n = 0\) there are no unitary divisors.

def unitaryDivisors (n : ℕ) : Finset ℕ :=
  n.divisors.filter fun d => d.Coprime (n / d)

Used by 24

Used byGreatest common unitary divisor · Symmetry of the greatest common unitary divisor · The greatest common unitary divisor divides its first argument · The greatest common unitary divisor divides its second argument · The greatest common unitary divisor is a common unitary divisor · Greatest common unitary divisor with zero on the left · Greatest common unitary divisor with zero on the right · Common unitary divisors are at most the greatest one · Morgado's formula as a sum over unitary divisors · Sum of unitary divisors · Gcd with a coprime factor preserves unitary divisors · The unitary convolution of multiplicative functions is multiplicative · Products of unitary divisors of coprime numbers · Unitary convolution · Unitary convolution as a sum over unitary divisors · Unitary convolution at prime powers · Unitary divisors of a prime power · Number of unitary divisors · Unitary divisor counts of unitary s-Zumkeller numbers · Unitary s-Zumkeller numbers · Lower bounds for unitary s-Zumkeller numbers · The number 60 is unitary s-Zumkeller · The number 6 is not unitary s-Zumkeller · Sum of squares of unitary divisors

DefinitionSum of unitary divisors#✓fully proved

For a natural number \(n\), \(\sigma^*(n)\) denotes the sum of the unitary divisors of \(n\).

def sigmaStar (n : ℕ) : ℕ :=
  ∑ d ∈ unitaryDivisors n, d

Uses 1

Statement usesUnitary divisors

Primitive elements

DefinitionElements primitive under divisibility#✓fully proved

Let \(S\) be a set of natural numbers. A natural number \(n\) is primitive in \(S\) under divisibility when \(n \in S\) and no proper divisor of \(n\), that is, no divisor \(d\) of \(n\) with \(d < n\), belongs to \(S\).

def IsPrimitiveByDivisibility (S : Set ℕ) (n : ℕ) : Prop :=
  n ∈ S ∧ Disjoint (n.properDivisors : Set ℕ) S

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.