Theorems · Theorem · number theory

ADEInequality.classification

∀ (p q r : ℕ+), 1 < ADEInequality.sumInv {p, q, r} ↔ ADEInequality.Admissible {p, q, r}

A multiset {p,q,r} of positive natural numbers is a solution to (p⁻¹ + q⁻¹ + r⁻¹ : ℚ) > 1 if and only if it is Admissible which means it is one of: * A' q r := {1,q,r} * D' r := {2,2,r} * E6 := {2,3,3}, or E7 := {2,3,4}, or E8 := {2,3,5}

Defined in

Mathlib.NumberTheory.ADEInequality

Cited by

0 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound