feat(linear_algebra/std_basis): add matrix.std_basis_eq_std_basis_mat…

…rix (#9216)

As suggested in #9072 by @eric-wieser, we modify `matrix.std_basis` to use the more familiar `n × m` as the index of the basis and we prove that the `(i,j)`-th element of this basis is `matrix.std_basis_matrix i j 1`.

src/linear_algebra/std_basis.lean

@@ -6,7 +6,7 @@ Authors: Johannes Hölzl
 import linear_algebra.basic
 import linear_algebra.basis
 import linear_algebra.pi
-import data.matrix.basic
+import data.matrix.basis
 
 /-!
 # The standard basis
@@ -251,13 +251,31 @@ by { simp only [basis_fun, basis.coe_of_equiv_fun, linear_equiv.refl_symm,
   (pi.basis_fun R η).repr x i = x i :=
 by simp [basis_fun]
 
-/-- The standard basis on `matrix n m R`. -/
-noncomputable def _root_.matrix.std_basis (n : Type*) (m : Type*) [fintype m] [fintype n] :
-  basis (Σ (j : n), (λ (i : n), m) j) R (matrix n m R) :=
-pi.basis (λ (i : n), pi.basis_fun R m)
-
 end
 
 end module
 
 end pi
+
+namespace matrix
+
+variables (R : Type*) (n : Type*) (m : Type*) [fintype m] [fintype n] [semiring R]
+
+/-- The standard basis of `matrix n m R`. -/
+noncomputable def std_basis : basis (n × m) R (matrix n m R) :=
+basis.reindex (pi.basis (λ (i : n), pi.basis_fun R m)) (equiv.sigma_equiv_prod _ _)
+
+variables {n m}
+
+lemma std_basis_eq_std_basis_matrix (i : n) (j : m) [decidable_eq n] [decidable_eq m] :
+  std_basis R n m (i, j) = std_basis_matrix i j (1 : R) :=
+begin
+  ext a b,
+  by_cases hi : i = a; by_cases hj : j = b,
+  { simp [std_basis, hi, hj] },
+  { simp [std_basis, hi, hj, ne.symm hj, linear_map.std_basis_ne] },
+  { simp [std_basis, hi, hj, ne.symm hi, linear_map.std_basis_ne] },
+  { simp [std_basis, hi, hj, ne.symm hj, ne.symm hi, linear_map.std_basis_ne] }
+end
+
+end matrix