Basic

@[inline]

def Fin.addCast {n : ℕ} (m : ℕ) : Fin n → Fin (m + n)

Imported declaration from the Incompleteness formalization.

Equations

• Fin.addCast m = Fin.castLE ⋯

@[simp]

theorem Fin.addCast_val {n m : ℕ} (i : Fin n) : ↑(addCast m i) = ↑i

@[simp]

theorem Matrix.appeendr_addCast {α : Type u_1} {m n : ℕ} (u : Fin m → α) (v : Fin n → α) (i : Fin m) : appendr u v (Fin.addCast n i) = u i

@[simp]

theorem Matrix.appeendr_addNat {α : Type u_1} {m n : ℕ} (u : Fin m → α) (v : Fin n → α) (i : Fin n) : appendr u v (i.addNat m) = v i