Biunitary divisors

DefinitionGreatest common unitary divisor#✓fully proved

For natural numbers \(a\) and \(b\), \(\gcd_1(a, b)\) is the largest natural number that is a unitary divisor of both \(a\) and \(b\), where a unitary divisor of \(n\) is a divisor \(d\) of \(n \neq 0\) with \(\gcd(d, n / d) = 1\). If \(a = 0\) or \(b = 0\), there is no common unitary divisor and \(\gcd_1(a, b) = 0\).

def gcdUnitary (a b : ℕ) : ℕ :=
  (a.unitaryDivisors ∩ b.unitaryDivisors).sup id
Sources
  • Tomohiro Yamada, Determining all Biunitary Triperfect Numbers of a Certain Form, Journal of Integer Sequences 28 (2025), Article 25.4.5, Section 1 (after Wall).
Uses 1 · Used by 12
Statement usesUnitary divisors
Used byBiunitary divisors · Zero has no biunitary divisors · Biunitary divisors divide · 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 · Positivity of the greatest 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 · Characterization of biunitary divisors

TheoremSymmetry of the greatest common unitary divisor#✓fully proved

For all natural numbers \(a\) and \(b\), the greatest common unitary divisor satisfies \(\gcd_1(a, b) = \gcd_1(b, a)\).

theorem gcdUnitary_comm (a b : ℕ) : gcdUnitary a b = gcdUnitary b a
Sources
  • Tomohiro Yamada, Determining all Biunitary Triperfect Numbers of a Certain Form, Journal of Integer Sequences 28 (2025), Article 25.4.5, Section 1 (after Wall).
Uses 2
Statement usesGreatest common unitary divisor
Proof usesUnitary divisors

TheoremGreatest common unitary divisor with zero on the left#✓fully proved

For every natural number \(b\), the greatest common unitary divisor satisfies \(\gcd_1(0, b) = 0\), since \(0\) has no unitary divisors.

@[simp]
theorem gcdUnitary_zero_left (b : ℕ) : gcdUnitary 0 b = 0
Sources
  • Tomohiro Yamada, Determining all Biunitary Triperfect Numbers of a Certain Form, Journal of Integer Sequences 28 (2025), Article 25.4.5, Section 1 (after Wall).
Uses 2
Statement usesGreatest common unitary divisor
Proof usesUnitary divisors

TheoremGreatest common unitary divisor with zero on the right#✓fully proved

For every natural number \(a\), the greatest common unitary divisor satisfies \(\gcd_1(a, 0) = 0\), since \(0\) has no unitary divisors.

@[simp]
theorem gcdUnitary_zero_right (a : ℕ) : gcdUnitary a 0 = 0
Sources
  • Tomohiro Yamada, Determining all Biunitary Triperfect Numbers of a Certain Form, Journal of Integer Sequences 28 (2025), Article 25.4.5, Section 1 (after Wall).
Uses 2 · Used by 1
Statement usesGreatest common unitary divisor
Proof usesUnitary divisors
Used byZero has no biunitary divisors

TheoremCommon unitary divisors are at most the greatest one#✓fully proved

For natural numbers \(a\), \(b\) and \(d\), if \(d\) is a unitary divisor of both \(a\) and \(b\), then \(d \le \gcd_1(a, b)\), where \(\gcd_1(a, b)\) is the greatest common unitary divisor of \(a\) and \(b\).

theorem le_gcdUnitary {a b d : ℕ} (ha : d ∈ a.unitaryDivisors) (hb : d ∈ b.unitaryDivisors) :
    d ≤ gcdUnitary a b
Sources
  • Tomohiro Yamada, Determining all Biunitary Triperfect Numbers of a Certain Form, Journal of Integer Sequences 28 (2025), Article 25.4.5, Section 1 (after Wall).
Uses 2
Statement usesGreatest common unitary divisor · Unitary divisors

TheoremThe greatest common unitary divisor is a common unitary divisor#✓fully proved

For positive natural numbers \(a\) and \(b\), the greatest common unitary divisor \(\gcd_1(a, b)\) is a unitary divisor of \(a\) and a unitary divisor of \(b\).

theorem gcdUnitary_mem_unitaryDivisors {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
    gcdUnitary a b ∈ a.unitaryDivisors ∧ gcdUnitary a b ∈ b.unitaryDivisors
Sources
  • Tomohiro Yamada, Determining all Biunitary Triperfect Numbers of a Certain Form, Journal of Integer Sequences 28 (2025), Article 25.4.5, Section 1 (after Wall).
Uses 2 · Used by 2
Statement usesGreatest common unitary divisor · Unitary divisors
Used byThe greatest common unitary divisor divides its first argument · The greatest common unitary divisor divides its second argument

TheoremThe greatest common unitary divisor divides its first argument#✓fully proved

For positive natural numbers \(a\) and \(b\), the greatest common unitary divisor \(\gcd_1(a, b)\) divides \(a\).

theorem gcdUnitary_dvd_left {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : gcdUnitary a b ∣ a
Sources
  • Tomohiro Yamada, Determining all Biunitary Triperfect Numbers of a Certain Form, Journal of Integer Sequences 28 (2025), Article 25.4.5, Section 1 (after Wall).
Uses 3 · Used by 1
Statement usesGreatest common unitary divisor
Proof usesThe greatest common unitary divisor is a common unitary divisor · Unitary divisors
Used byPositivity of the greatest common unitary divisor

TheoremThe greatest common unitary divisor divides its second argument#✓fully proved

For positive natural numbers \(a\) and \(b\), the greatest common unitary divisor \(\gcd_1(a, b)\) divides \(b\).

theorem gcdUnitary_dvd_right {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : gcdUnitary a b ∣ b
Sources
  • Tomohiro Yamada, Determining all Biunitary Triperfect Numbers of a Certain Form, Journal of Integer Sequences 28 (2025), Article 25.4.5, Section 1 (after Wall).
Uses 3
Statement usesGreatest common unitary divisor
Proof usesThe greatest common unitary divisor is a common unitary divisor · Unitary divisors

TheoremPositivity of the greatest common unitary divisor#✓fully proved

For positive natural numbers \(a\) and \(b\), the greatest common unitary divisor \(\gcd_1(a, b)\) is positive.

theorem gcdUnitary_pos {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : 0 < gcdUnitary a b
Sources
  • Tomohiro Yamada, Determining all Biunitary Triperfect Numbers of a Certain Form, Journal of Integer Sequences 28 (2025), Article 25.4.5, Section 1 (after Wall).
Uses 2
Statement usesGreatest common unitary divisor
Proof usesThe greatest common unitary divisor divides its first argument

DefinitionBiunitary divisors#✓fully proved

For a natural number \(n\), the biunitary divisors of \(n\) are the divisors \(d\) of \(n\) with \(\gcd_1(d, n/d) = 1\), where \(\gcd_1(a, b)\) denotes the greatest common unitary divisor of \(a\) and \(b\). For \(n = 0\) the set is empty.

def biunitaryDivisors (n : ℕ) : Finset ℕ :=
  n.divisors.filter fun d => gcdUnitary d (n / d) = 1
Sources
  • Tomohiro Yamada, Determining all Biunitary Triperfect Numbers of a Certain Form, Journal of Integer Sequences 28 (2025), Article 25.4.5, Section 1 (after Wall).
Uses 1 · Used by 5
Statement usesGreatest common unitary divisor
Used byZero has no biunitary divisors · Biunitary divisors divide · Characterization of biunitary divisors · Biunitary divisor sum · The biunitary divisor sum of \(0\)

DefinitionBiunitary divisor sum#✓fully proved

For a natural number \(n\), \(\sigma^{**}(n)\) is the sum of the biunitary divisors of \(n\), that is, of the divisors \(d\) of \(n\) with \(\gcd_1(d, n / d) = 1\), where \(\gcd_1\) denotes the greatest common unitary divisor. Since \(0\) has no biunitary divisors, \(\sigma^{**}(0) = 0\).

def sigmaBiunitary (n : ℕ) : ℕ :=
  ∑ d ∈ biunitaryDivisors n, d
Sources
  • Tomohiro Yamada, Determining all Biunitary Triperfect Numbers of a Certain Form, Journal of Integer Sequences 28 (2025), Article 25.4.5, Section 1 (after Wall).
Uses 1 · Used by 25
Statement usesBiunitary divisors
Used byThe biunitary divisor sum of \(4\) · The biunitary divisor sum of \(1\) · \(120\) is biunitary triperfect · The biunitary divisor sum of \(16\) · The biunitary divisor sum of \(27\) · The biunitary divisor sum of \(0\) · Biunitary triperfect numbers exactly divisible by \(2^4\) and by \(3^3\) or \(3^4\) · Prime factors of the biunitary divisor sum of \(41^g\) · Prime factors at least \(5\) of biunitary divisor sums of prime powers · Prime factors at least \(7\) of biunitary divisor sums of odd prime powers · Two prime factors of the biunitary divisor sum of \(13^g\) · No biunitary triperfect number divisible by \(27\) is exactly divisible by \(2^5\) · No biunitary triperfect number divisible by \(27\) is exactly divisible by \(2^6\) · Biunitary triperfect numbers divisible by \(27\) are divisible by \(16\) · Biunitary triperfect numbers exactly divisible by \(2^4\) and divisible by \(3^5\) are prime to \(5\) · No biunitary triperfect number has \(3\)-exponent \(3\) and \(2\)-exponent at least \(7\) · No biunitary triperfect number has \(3\)-exponent \(4\) and \(2\)-exponent at least \(7\) · Parity of the biunitary divisor sum · The only biunitary triperfect number divisible by \(27\) is \(2160\) · Lower bounds for the biunitary divisor sum of a prime power · Comparison bounds for the biunitary divisor sum of a prime power · Prime factors of the biunitary divisor sum of a power of \(3\) · Prime factors of the biunitary divisor sum of a power of \(2\) · Powers of two dividing the biunitary divisor sum of an odd number · Divisibility of the biunitary divisor sum of an even number by a power of two

TheoremCharacterization of biunitary divisors#✓fully proved

For natural numbers \(n\) and \(d\), \(d\) is a biunitary divisor of \(n\) if and only if \(d\) divides \(n\), \(n \neq 0\) and \(\gcd_1(d, n / d) = 1\), where \(\gcd_1\) denotes the greatest common unitary divisor.

@[simp]
theorem mem_biunitaryDivisors {n d : ℕ} :
    d ∈ biunitaryDivisors n ↔ d ∣ n ∧ n ≠ 0 ∧ gcdUnitary d (n / d) = 1
Sources
  • Tomohiro Yamada, Determining all Biunitary Triperfect Numbers of a Certain Form, Journal of Integer Sequences 28 (2025), Article 25.4.5, Section 1 (after Wall).
Uses 2 · Used by 1
Statement usesBiunitary divisors · Greatest common unitary divisor
Used byBiunitary divisors divide

TheoremZero has no biunitary divisors#✓fully proved

The set of biunitary divisors of \(0\) is empty.

@[simp]
theorem biunitaryDivisors_zero : biunitaryDivisors 0 = ∅
Sources
  • Tomohiro Yamada, Determining all Biunitary Triperfect Numbers of a Certain Form, Journal of Integer Sequences 28 (2025), Article 25.4.5, Section 1 (after Wall).
Uses 3 · Used by 1
Statement usesBiunitary divisors
Proof usesGreatest common unitary divisor · Greatest common unitary divisor with zero on the right
Used byThe biunitary divisor sum of \(0\)

TheoremThe biunitary divisor sum of \(0\)#✓fully proved

The sum \(\sigma^{**}(0)\) of the biunitary divisors of \(0\) equals \(0\).

@[simp]
theorem sigmaBiunitary_zero : sigmaBiunitary 0 = 0
Sources
  • Tomohiro Yamada, Determining all Biunitary Triperfect Numbers of a Certain Form, Journal of Integer Sequences 28 (2025), Article 25.4.5, Section 1 (after Wall).
Uses 3
Statement usesBiunitary divisor sum
Proof usesBiunitary divisors · Zero has no biunitary divisors

TheoremBiunitary divisors divide#✓fully proved

For natural numbers \(n\) and \(d\), if \(d\) is a biunitary divisor of \(n\), then \(d\) divides \(n\).

theorem dvd_of_mem_biunitaryDivisors {n d : ℕ} (h : d ∈ biunitaryDivisors n) : d ∣ n
Sources
  • Tomohiro Yamada, Determining all Biunitary Triperfect Numbers of a Certain Form, Journal of Integer Sequences 28 (2025), Article 25.4.5, Section 1 (after Wall).
Uses 3
Statement usesBiunitary divisors
Proof usesGreatest common unitary divisor · Characterization of biunitary divisors

TheoremThe biunitary divisor sum of \(1\)#✓fully proved

The sum \(\sigma^{**}(1)\) of the biunitary divisors of \(1\) equals \(1\).

theorem sigmaBiunitary_one : sigmaBiunitary 1 = 1
Sources
  • Tomohiro Yamada, Determining all Biunitary Triperfect Numbers of a Certain Form, Journal of Integer Sequences 28 (2025), Article 25.4.5, Section 1 (after Wall).
Uses 1
Statement usesBiunitary divisor sum

TheoremThe biunitary divisor sum of \(4\)#✓fully proved

The sum \(\sigma^{**}(4)\) of the biunitary divisors of \(4\) equals \(5\).

The biunitary divisors of \(4\) are \(1\) and \(4\): the divisor \(2\) is not biunitary, since the greatest common unitary divisor of \(2\) and \(2\) is \(2\).

theorem sigmaBiunitary_four : sigmaBiunitary 4 = 5
Sources
  • Tomohiro Yamada, Determining all Biunitary Triperfect Numbers of a Certain Form, Journal of Integer Sequences 28 (2025), Article 25.4.5, Lemma 3.1 (σ**(2²) = 5).
Uses 1
Statement usesBiunitary divisor sum

TheoremThe biunitary divisor sum of \(16\)#✓fully proved

The sum \(\sigma^{**}(16)\) of the biunitary divisors of \(16\) equals \(1 + 2 + 8 + 16 = 27\).

theorem sigmaBiunitary_sixteen : sigmaBiunitary 16 = 27
Sources
  • Tomohiro Yamada, Determining all Biunitary Triperfect Numbers of a Certain Form, Journal of Integer Sequences 28 (2025), Article 25.4.5, formula (1) at p = 2, e = 4.
Uses 1
Statement usesBiunitary divisor sum

TheoremThe biunitary divisor sum of \(27\)#✓fully proved

The sum \(\sigma^{**}(27)\) of the biunitary divisors of \(27\) equals \(1 + 3 + 9 + 27 = 40\).

theorem sigmaBiunitary_twentySeven : sigmaBiunitary 27 = 40
Sources
  • Tomohiro Yamada, Determining all Biunitary Triperfect Numbers of a Certain Form, Journal of Integer Sequences 28 (2025), Article 25.4.5, Lemma 3.6 (σ**(3³) = 2³ · 5).
Uses 1
Statement usesBiunitary divisor sum

Theorem\(120\) is biunitary triperfect#✓fully proved

The sum \(\sigma^{**}(120)\) of the biunitary divisors of \(120\) equals \(3 \cdot 120 = 360\).

theorem sigmaBiunitary_oneHundredTwenty : sigmaBiunitary 120 = 3 * 120
Sources
  • Tomohiro Yamada, Determining all Biunitary Triperfect Numbers of a Certain Form, Journal of Integer Sequences 28 (2025), Article 25.4.5, Section 1 (smallest instances 120, 672, 2160 with k = 3).
Uses 1
Statement usesBiunitary divisor sum
20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.