[STATEMENT]
lemma matrix_right_invertible_ker:
  fixes M :: "real^('m::finite)^'n"
  shows "(\<exists> M'. M ** M' = mat 1) \<longleftrightarrow> (\<forall> x. x v* M = 0 \<longrightarrow> x = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>M'. M ** M' = mat 1) = (\<forall>x. x v* M = 0 \<longrightarrow> x = 0)
[PROOF STEP]
using left_invertible_transpose matrix_left_invertible_ker
[PROOF STATE]
proof (prove)
using this:
(\<exists>B. B ** Finite_Cartesian_Product.transpose ?A = mat (1::?'a)) = (\<exists>B. ?A ** B = mat (1::?'a))
(\<exists>B. B ** ?A = mat (1::?'a)) = (\<forall>x. ?A *v x = 0 \<longrightarrow> x = 0)

goal (1 subgoal):
 1. (\<exists>M'. M ** M' = mat 1) = (\<forall>x. x v* M = 0 \<longrightarrow> x = 0)
[PROOF STEP]
by force