chore(*/matrix): order m and n alphabetically (#13510)

In a few places this also reorders `(n) [fintype n] (m) [fintype m]` to `(m n) [fintype m] [fintype n]` which seems to be where we prefer to put typeclasses.

src/analysis/matrix.lean

@@ -24,40 +24,40 @@ open_locale nnreal
 
 namespace matrix
 
-variables {R n m α : Type*} [fintype n] [fintype m]
+variables {R m n α : Type*} [fintype m] [fintype n]
 
 section semi_normed_group
 variables [semi_normed_group α]
 
 /-- Seminormed group instance (using sup norm of sup norm) for matrices over a seminormed ring. Not
 declared as an instance because there are several natural choices for defining the norm of a
 matrix. -/
-protected def semi_normed_group : semi_normed_group (matrix n m α) :=
+protected def semi_normed_group : semi_normed_group (matrix m n α) :=
 pi.semi_normed_group
 
 local attribute [instance] matrix.semi_normed_group
 
-lemma norm_le_iff {r : ℝ} (hr : 0 ≤ r) {A : matrix n m α} :
+lemma norm_le_iff {r : ℝ} (hr : 0 ≤ r) {A : matrix m n α} :
   ∥A∥ ≤ r ↔ ∀ i j, ∥A i j∥ ≤ r :=
 by simp [pi_norm_le_iff hr]
 
-lemma nnnorm_le_iff {r : ℝ≥0} {A : matrix n m α} :
+lemma nnnorm_le_iff {r : ℝ≥0} {A : matrix m n α} :
   ∥A∥₊ ≤ r ↔ ∀ i j, ∥A i j∥₊ ≤ r :=
 by simp [pi_nnnorm_le_iff]
 
-lemma norm_lt_iff {r : ℝ} (hr : 0 < r) {A : matrix n m α} :
+lemma norm_lt_iff {r : ℝ} (hr : 0 < r) {A : matrix m n α} :
   ∥A∥ < r ↔ ∀ i j, ∥A i j∥ < r :=
 by simp [pi_norm_lt_iff hr]
 
-lemma nnnorm_lt_iff {r : ℝ≥0} (hr : 0 < r) {A : matrix n m α} :
+lemma nnnorm_lt_iff {r : ℝ≥0} (hr : 0 < r) {A : matrix m n α} :
   ∥A∥₊ < r ↔ ∀ i j, ∥A i j∥₊ < r :=
 by simp [pi_nnnorm_lt_iff hr]
 
-lemma norm_entry_le_entrywise_sup_norm (A : matrix n m α) {i : n} {j : m} :
+lemma norm_entry_le_entrywise_sup_norm (A : matrix m n α) {i : m} {j : n} :
   ∥A i j∥ ≤ ∥A∥ :=
 (norm_le_pi_norm (A i) j).trans (norm_le_pi_norm A i)
 
-lemma nnnorm_entry_le_entrywise_sup_nnorm (A : matrix n m α) {i : n} {j : m} :
+lemma nnnorm_entry_le_entrywise_sup_nnorm (A : matrix m n α) {i : m} {j : n} :
   ∥A i j∥₊ ≤ ∥A∥₊ :=
 (nnnorm_le_pi_nnnorm (A i) j).trans (nnnorm_le_pi_nnnorm A i)
 
@@ -66,7 +66,7 @@ end semi_normed_group
 /-- Normed group instance (using sup norm of sup norm) for matrices over a normed ring.  Not
 declared as an instance because there are several natural choices for defining the norm of a
 matrix. -/
-protected def normed_group [normed_group α] : normed_group (matrix n m α) :=
+protected def normed_group [normed_group α] : normed_group (matrix m n α) :=
 pi.normed_group
 
 section normed_space
@@ -77,7 +77,7 @@ variables [normed_field R] [semi_normed_group α] [normed_space R α]
 /-- Normed space instance (using sup norm of sup norm) for matrices over a normed field.  Not
 declared as an instance because there are several natural choices for defining the norm of a
 matrix. -/
-protected def normed_space : normed_space R (matrix n m α) :=
+protected def normed_space : normed_space R (matrix m n α) :=
 pi.normed_space
 
 end normed_space

src/data/matrix/basic.lean

@@ -1052,8 +1052,8 @@ lemma add_vec_mul [fintype m] (A : matrix m n α) (x y : m → α) :
   vec_mul (x + y) A = vec_mul x A + vec_mul y A :=
 by { ext, apply add_dot_product }
 
-lemma vec_mul_smul [fintype n] [comm_semiring R] [semiring S] [algebra R S]
-  (M : matrix n m S) (b : R) (v : n → S)  :
+lemma vec_mul_smul [fintype m] [comm_semiring R] [semiring S] [algebra R S]
+  (M : matrix m n S) (b : R) (v : m → S)  :
   M.vec_mul (b • v) = b • M.vec_mul v :=
 by { ext i, simp only [vec_mul, dot_product, finset.smul_sum, pi.smul_apply, smul_mul_assoc] }
 
@@ -1485,8 +1485,8 @@ lemma conj_transpose_reindex [has_star α] (eₘ : m ≃ l) (eₙ : n ≃ o) (M
 rfl
 
 @[simp]
-lemma minor_mul_transpose_minor [fintype n] [fintype m] [semiring α]
-  (e : n ≃ m) (M : matrix n m α) :
+lemma minor_mul_transpose_minor [fintype m] [fintype n] [semiring α]
+  (e : m ≃ n) (M : matrix m n α) :
   (M.minor id e) ⬝ (Mᵀ).minor e id = M ⬝ Mᵀ :=
 by rw [minor_mul_equiv, minor_id_id]
 
@@ -1581,98 +1581,98 @@ end row_col
 section update
 
 /-- Update, i.e. replace the `i`th row of matrix `A` with the values in `b`. -/
-def update_row [decidable_eq n] (M : matrix n m α) (i : n) (b : m → α) : matrix n m α :=
+def update_row [decidable_eq m] (M : matrix m n α) (i : m) (b : n → α) : matrix m n α :=
 function.update M i b
 
 /-- Update, i.e. replace the `j`th column of matrix `A` with the values in `b`. -/
-def update_column [decidable_eq m] (M : matrix n m α) (j : m) (b : n → α) : matrix n m α :=
+def update_column [decidable_eq n] (M : matrix m n α) (j : n) (b : m → α) : matrix m n α :=
 λ i, function.update (M i) j (b i)
 
-variables {M : matrix n m α} {i : n} {j : m} {b : m → α} {c : n → α}
+variables {M : matrix m n α} {i : m} {j : n} {b : n → α} {c : m → α}
 
-@[simp] lemma update_row_self [decidable_eq n] : update_row M i b i = b :=
+@[simp] lemma update_row_self [decidable_eq m] : update_row M i b i = b :=
 function.update_same i b M
 
-@[simp] lemma update_column_self [decidable_eq m] : update_column M j c i j = c i :=
+@[simp] lemma update_column_self [decidable_eq n] : update_column M j c i j = c i :=
 function.update_same j (c i) (M i)
 
-@[simp] lemma update_row_ne [decidable_eq n] {i' : n} (i_ne : i' ≠ i) :
+@[simp] lemma update_row_ne [decidable_eq m] {i' : m} (i_ne : i' ≠ i) :
   update_row M i b i' = M i' := function.update_noteq i_ne b M
 
-@[simp] lemma update_column_ne [decidable_eq m] {j' : m} (j_ne : j' ≠ j) :
+@[simp] lemma update_column_ne [decidable_eq n] {j' : n} (j_ne : j' ≠ j) :
   update_column M j c i j' = M i j' := function.update_noteq j_ne (c i) (M i)
 
-lemma update_row_apply [decidable_eq n] {i' : n} :
+lemma update_row_apply [decidable_eq m] {i' : m} :
   update_row M i b i' j = if i' = i then b j else M i' j :=
 begin
   by_cases i' = i,
   { rw [h, update_row_self, if_pos rfl] },
   { rwa [update_row_ne h, if_neg h] }
 end
 
-lemma update_column_apply [decidable_eq m] {j' : m} :
+lemma update_column_apply [decidable_eq n] {j' : n} :
   update_column M j c i j' = if j' = j then c i else M i j' :=
 begin
   by_cases j' = j,
   { rw [h, update_column_self, if_pos rfl] },
   { rwa [update_column_ne h, if_neg h] }
 end
 
-@[simp] lemma update_column_subsingleton [subsingleton m] (A : matrix n m R)
-  (i : m) (b : n → R) :
-  A.update_column i b = (col b).minor id (function.const m ()) :=
+@[simp] lemma update_column_subsingleton [subsingleton n] (A : matrix m n R)
+  (i : n) (b : m → R) :
+  A.update_column i b = (col b).minor id (function.const n ()) :=
 begin
   ext x y,
   simp [update_column_apply, subsingleton.elim i y]
 end
 
-@[simp] lemma update_row_subsingleton [subsingleton n] (A : matrix n m R)
-  (i : n) (b : m → R)  :
-  A.update_row i b = (row b).minor (function.const n ()) id :=
+@[simp] lemma update_row_subsingleton [subsingleton m] (A : matrix m n R)
+  (i : m) (b : n → R)  :
+  A.update_row i b = (row b).minor (function.const m ()) id :=
 begin
   ext x y,
   simp [update_column_apply, subsingleton.elim i x]
 end
 
-lemma map_update_row [decidable_eq n] (f : α → β) :
+lemma map_update_row [decidable_eq m] (f : α → β) :
   map (update_row M i b) f = update_row (M.map f) i (f ∘ b) :=
 begin
   ext i' j',
   rw [update_row_apply, map_apply, map_apply, update_row_apply],
   exact apply_ite f _ _ _,
 end
 
-lemma map_update_column [decidable_eq m] (f : α → β) :
+lemma map_update_column [decidable_eq n] (f : α → β) :
   map (update_column M j c) f = update_column (M.map f) j (f ∘ c) :=
 begin
   ext i' j',
   rw [update_column_apply, map_apply, map_apply, update_column_apply],
   exact apply_ite f _ _ _,
 end
 
-lemma update_row_transpose [decidable_eq m] : update_row Mᵀ j c = (update_column M j c)ᵀ :=
+lemma update_row_transpose [decidable_eq n] : update_row Mᵀ j c = (update_column M j c)ᵀ :=
 begin
   ext i' j,
   rw [transpose_apply, update_row_apply, update_column_apply],
   refl
 end
 
-lemma update_column_transpose [decidable_eq n] : update_column Mᵀ i b = (update_row M i b)ᵀ :=
+lemma update_column_transpose [decidable_eq m] : update_column Mᵀ i b = (update_row M i b)ᵀ :=
 begin
   ext i' j,
   rw [transpose_apply, update_row_apply, update_column_apply],
   refl
 end
 
-lemma update_row_conj_transpose [decidable_eq m] [has_star α] :
+lemma update_row_conj_transpose [decidable_eq n] [has_star α] :
   update_row Mᴴ j (star c) = (update_column M j c)ᴴ :=
 begin
   rw [conj_transpose, conj_transpose, transpose_map, transpose_map, update_row_transpose,
     map_update_column],
   refl,
 end
 
-lemma update_column_conj_transpose [decidable_eq n] [has_star α] :
+lemma update_column_conj_transpose [decidable_eq m] [has_star α] :
   update_column Mᴴ i (star b) = (update_row M i b)ᴴ :=
 begin
   rw [conj_transpose, conj_transpose, transpose_map, transpose_map, update_column_transpose,

src/data/matrix/basis.lean

@@ -46,8 +46,8 @@ begin
   split_ifs with h; simp [h],
 end
 
-lemma matrix_eq_sum_std_basis (x : matrix n m α) [fintype n] [fintype m] :
-  x = ∑ (i : n) (j : m), std_basis_matrix i j (x i j) :=
+lemma matrix_eq_sum_std_basis [fintype m] [fintype n] (x : matrix m n α) :
+  x = ∑ (i : m) (j : n), std_basis_matrix i j (x i j) :=
 begin
   ext, symmetry,
   iterate 2 { rw finset.sum_apply },
@@ -62,7 +62,7 @@ end
 
 -- TODO: add `std_basis_vec`
 lemma std_basis_eq_basis_mul_basis (i : m) (j : n) :
-std_basis_matrix i j 1 = vec_mul_vec (λ i', ite (i = i') 1 0) (λ j', ite (j = j') 1 0) :=
+  std_basis_matrix i j 1 = vec_mul_vec (λ i', ite (i = i') 1 0) (λ j', ite (j = j') 1 0) :=
 begin
   ext,
   norm_num [std_basis_matrix, vec_mul_vec],

src/linear_algebra/free_module/basic.lean

@@ -97,9 +97,8 @@ instance pi {ι : Type*} [fintype ι] {M : ι → Type*} [Π (i : ι), add_comm_
 of_basis $ pi.basis $ λ i, choose_basis R (M i)
 
 /-- The module of finite matrices is free. -/
-instance matrix {n : Type*} [fintype n] {m : Type*} [fintype m] :
-  module.free R (matrix n m R) :=
-of_basis $ matrix.std_basis R n m
+instance matrix {m n : Type*} [fintype m] [fintype n] : module.free R (matrix m n R) :=
+of_basis $ matrix.std_basis R m n
 
 variables {R M N}
 

src/linear_algebra/free_module/finite/rank.lean

@@ -87,10 +87,10 @@ begin
     ← mk_sigma, mk_to_nat_eq_card, card_sigma],
 end
 
-/-- If `n` and `m` are `fintype`, the finrank of `n × m` matrices is
-  `(fintype.card n) * (fintype.card m)`. -/
-lemma finrank_matrix (n : Type v) [fintype n] (m : Type w) [fintype m] :
-  finrank R (matrix n m R) = (card n) * (card m) :=
+/-- If `m` and `n` are `fintype`, the finrank of `m × n` matrices is
+  `(fintype.card m) * (fintype.card n)`. -/
+lemma finrank_matrix (m n : Type v) [fintype m] [fintype n] :
+  finrank R (matrix m n R) = (card m) * (card n) :=
 by { simp [finrank] }
 
 end ring

src/linear_algebra/free_module/rank.lean

@@ -70,25 +70,25 @@ end
   module.rank R (Π i, M i) = cardinal.sum (λ i, module.rank R (M i)) :=
 by { rw [← (direct_sum.linear_equiv_fun_on_fintype _ _ M).dim_eq, rank_direct_sum] }
 
-/-- If `n` and `m` are `fintype`, the rank of `n × m` matrices is `(# n).lift * (# m).lift`. -/
-@[simp] lemma rank_matrix (n : Type v) [fintype n] (m : Type w) [fintype m] :
-  module.rank R (matrix n m R) = (lift.{(max v w u) v} (# n)) * (lift.{(max v w u) w} (# m)) :=
+/-- If `m` and `n` are `fintype`, the rank of `m × n` matrices is `(# m).lift * (# n).lift`. -/
+@[simp] lemma rank_matrix (m : Type v) (n : Type w) [fintype m] [fintype n] :
+  module.rank R (matrix m n R) = (lift.{(max v w u) v} (# m)) * (lift.{(max v w u) w} (# n)) :=
 begin
-  have h := (matrix.std_basis R n m).mk_eq_dim,
+  have h := (matrix.std_basis R m n).mk_eq_dim,
   rw [← lift_lift.{(max v w u) (max v w)}, lift_inj] at h,
   simpa using h.symm,
 end
 
-/-- If `n` and `m` are `fintype` that lie in the same universe, the rank of `n × m` matrices is
+/-- If `m` and `n` are `fintype` that lie in the same universe, the rank of `m × n` matrices is
   `(# n * # m).lift`. -/
-@[simp] lemma rank_matrix' (n : Type v) [fintype n] (m : Type v) [fintype m] :
-  module.rank R (matrix n m R) =  (# n * # m).lift :=
+@[simp] lemma rank_matrix' (m n : Type v) [fintype m] [fintype n] :
+  module.rank R (matrix m n R) =  (# m * # n).lift :=
 by rw [rank_matrix, lift_mul, lift_umax]
 
-/-- If `n` and `m` are `fintype` that lie in the same universe as `R`, the rank of `n × m` matrices
-  is `# n * # m`. -/
-@[simp] lemma rank_matrix'' (n : Type u) [fintype n] (m : Type u) [fintype m] :
-  module.rank R (matrix n m R) =  # n * # m := by simp
+/-- If `m` and `n` are `fintype` that lie in the same universe as `R`, the rank of `m × n` matrices
+  is `# m * # n`. -/
+@[simp] lemma rank_matrix'' (m n : Type u) [fintype m] [fintype n] :
+  module.rank R (matrix m n R) =  # m * # n := by simp
 
 end ring
 

src/linear_algebra/matrix/to_lin.lean

@@ -26,8 +26,8 @@ types used for indexing.
  * `linear_map.to_matrix`: given bases `v₁ : ι → M₁` and `v₂ : κ → M₂`,
    the `R`-linear equivalence from `M₁ →ₗ[R] M₂` to `matrix κ ι R`
  * `matrix.to_lin`: the inverse of `linear_map.to_matrix`
- * `linear_map.to_matrix'`: the `R`-linear equivalence from `(n → R) →ₗ[R] (m → R)`
-   to `matrix n m R` (with the standard basis on `n → R` and `m → R`)
+ * `linear_map.to_matrix'`: the `R`-linear equivalence from `(m → R) →ₗ[R] (n → R)`
+   to `matrix m n R` (with the standard basis on `m → R` and `n → R`)
  * `matrix.to_lin'`: the inverse of `linear_map.to_matrix'`
  * `alg_equiv_matrix`: given a basis indexed by `n`, the `R`-algebra equivalence between
    `R`-endomorphisms of `M` and `matrix n n R`

src/linear_algebra/std_basis.lean

@@ -262,11 +262,11 @@ end pi
 
 namespace matrix
 
-variables (R : Type*) (n : Type*) (m : Type*) [fintype m] [fintype n] [semiring R]
+variables (R : Type*) (m n : 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 _ _)
+/-- The standard basis of `matrix m n R`. -/
+noncomputable def std_basis : basis (m × n) R (matrix m n R) :=
+basis.reindex (pi.basis (λ (i : m), pi.basis_fun R n)) (equiv.sigma_equiv_prod _ _)
 
 variables {n m}
 

src/topology/algebra/matrix.lean

@@ -45,19 +45,19 @@ lemma continuous.matrix_elem {A : X → matrix m n R} (hA : continuous A) (i : m
 (continuous_apply_apply i j).comp hA
 
 @[continuity]
-lemma continuous.matrix_map [topological_space S] {A : X → matrix n m S} {f : S → R}
+lemma continuous.matrix_map [topological_space S] {A : X → matrix m n S} {f : S → R}
    (hA : continuous A) (hf : continuous f) :
   continuous (λ x, (A x).map f) :=
 continuous_matrix $ λ i j, hf.comp $ hA.matrix_elem _ _
 
 @[continuity]
-lemma continuous.matrix_transpose {A : X → matrix n m R} (hA : continuous A) :
+lemma continuous.matrix_transpose {A : X → matrix m n R} (hA : continuous A) :
   continuous (λ x, (A x)ᵀ) :=
 continuous_matrix $ λ i j, hA.matrix_elem j i
 
 /-! TODO: add a `has_continuous_star` typeclass so we can write
 ```
-lemma continuous.matrix.conj_transpose [has_star R] {A : X → matrix n m R} (hA : continuous A) :
+lemma continuous.matrix.conj_transpose [has_star R] {A : X → matrix m n R} (hA : continuous A) :
   continuous (λ x, (A x)ᴴ) :=
 hA.matrix_transpose.matrix_map continuous_star
 ```