def Nat.natToVec : ℕ → (n : ℕ) → Option (Fin n → ℕ)

Equations

• Nat.natToVec 0 0 = some ![]
• e.succ.natToVec n.succ = Option.map (fun (x : Fin n → ℕ) => (Nat.unpair e).1 :> x) ((Nat.unpair e).2.natToVec n)
• x✝¹.natToVec x✝ = none

@[simp]

theorem Nat.natToVec_vecToNat {n : ℕ} (v : Fin n → ℕ) : (Matrix.vecToNat v).natToVec n = some v

theorem Nat.lt_of_eq_natToVec {n e : ℕ} {v : Fin n → ℕ} (h : e.natToVec n = some v) (i : Fin n) : v i < e