[STATEMENT]
lemma row_zero[simp]:
  "i < nr \<Longrightarrow> row (0\<^sub>m nr nc) i = 0\<^sub>v nc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < nr \<Longrightarrow> row (0\<^sub>m nr nc) i = 0\<^sub>v nc
[PROOF STEP]
by (intro eq_vecI, auto)