@[simp]
theorem
Matrix.appeendr_addCast
{α : Type u_1}
{m : ℕ}
{n : ℕ}
(u : Fin m → α)
(v : Fin n → α)
(i : Fin m)
:
Matrix.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)
:
Matrix.appendr u v (i.addNat m) = v i