Amicable numbers

Two natural numbers $a$ and $b$ are amicable if $\sigma(a) = \sigma(b) = a + b$, where $\sigma$ is the sum-of-divisors function.

structure IsAmicable (a b : ℕ) : Prop

We say that $a,b\in \mathbb{N}$ are an amicable pair if $\sigma(a)=\sigma(b)=a+b$.

• left : (ArithmeticFunction.sigma 1) a = a + b
• right : (ArithmeticFunction.sigma 1) b = a + b

theorem isAmicable_iff (a b : ℕ) : IsAmicable a b ↔ (ArithmeticFunction.sigma 1) a = a + b ∧ (ArithmeticFunction.sigma 1) b = a + b