SplitArithmetic.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.unit_fraction_split line 9
Source documentation
Splitting a positive unit fraction into the two usual larger fractions.
```
theorem unit_fraction_split (n : ℕ) (hn : 0 < n) :
    (1 : ℚ) / n = 1 / (n + 1 : ℕ) + 1 / (n * (n + 1) : ℕ) := by
…
```
theorem OAI.Problem337.composite_unit_fraction_split line 19
Source documentation
A composite denominator admits a split strictly between the two exceptional denominators for ordinary unit-fraction splitting.
```
theorem composite_unit_fraction_split (n : ℕ) (hn : 2 ≤ n)
    (hp : ¬ Nat.Prime n) :
    ∃ u v : ℕ, n + 1 < u ∧ u < v ∧ v < n * (n + 1) ∧
      (1 : ℚ) / n = 1 / u + 1 / v := by
…
```
Mentions: OAI.Problem337.v