Permutation Tables
Prove that there exist infinitely many tables with $3$ rows and $n$ columns containing exactly numbers from $1$ to $3n$ such that the third row is the component-wise sum of the first two rows. The number of columns $n$ may vary.
_Replace_ `sorry` _in the template below with your solution. Mathlib version used by the checker is v4.28.0_.
import Mathlib.Data.Fintype.Basic
import Mathlib.Order.Interval.Finset.Nat
structure Table (n : ℕ) where
row1 : ℕ → ℕ
row2 : ℕ → ℕ
row3 : ℕ → ℕ
def Table.valid {n : ℕ} (T : Table n) : Prop :=
∀ j ∈ Finset.Icc 1 n, T.row3 j = T.row1 j + T.row2 j
def Table.range {n : ℕ} (T : Table n) : Finset ℕ :=
(Finset.Icc 1 n).image T.row1 ∪
(Finset.Icc 1 n).image T.row2 ∪
(Finset.Icc 1 n).image T.row3
def Table.permutation {n : ℕ} (T : Table n) : Prop :=
T.range = Finset.Icc 1 (3 * n)
theorem solution : ∀ N : ℕ, ∃ n ≥ N, ∃ T : Table n, T.valid ∧ T.permutation := sorry
Submit Solution
Login to submit a solution.
Recent Submissions
| # | User | Time (UTC) | Status |
|---|---|---|---|
| 54 | cwrv | Long time ago | PASSED ⓘ |
| 42 | Kitsune | Long time ago | PASSED ⓘ |