chore(data/matrix/basic): rename _val lemmas to _apply (#3297)

We use `_apply` for lemmas about applications of functions to arguments. Arguably "picking out the entries of a matrix" could warrant a different name, but as we treat matrices just as functions all over, I think it's better to use the usual names.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Author: kim-em

src/algebra/classical_lie_algebras.lean

@@ -124,7 +124,7 @@ begin
   let B := Eb R j i hij.symm,
   intros c,
   have c' : A.val ⬝ B.val = B.val ⬝ A.val := by { rw [←sub_eq_zero, ←sl_bracket, c.abelian], refl, },
-  have : (1 : R) = 0 := by simpa [matrix.mul_val, hij] using (congr_fun (congr_fun c' i) i),
+  have : (1 : R) = 0 := by simpa [matrix.mul_apply, hij] using (congr_fun (congr_fun c' i) i),
   exact one_ne_zero this,
 end
 

src/data/matrix/basic.lean

@@ -64,9 +64,9 @@ instance [has_neg α] : has_neg (matrix m n α) := pi.has_neg
 instance [add_group α] : add_group (matrix m n α) := pi.add_group
 instance [add_comm_group α] : add_comm_group (matrix m n α) := pi.add_comm_group
 
-@[simp] theorem zero_val [has_zero α] (i j) : (0 : matrix m n α) i j = 0 := rfl
-@[simp] theorem neg_val [has_neg α] (M : matrix m n α) (i j) : (- M) i j = - M i j := rfl
-@[simp] theorem add_val [has_add α] (M N : matrix m n α) (i j) : (M + N) i j = M i j + N i j := rfl
+@[simp] theorem zero_apply [has_zero α] (i j) : (0 : matrix m n α) i j = 0 := rfl
+@[simp] theorem neg_apply [has_neg α] (M : matrix m n α) (i j) : (- M) i j = - M i j := rfl
+@[simp] theorem add_apply [has_add α] (M N : matrix m n α) (i j) : (M + N) i j = M i j + N i j := rfl
 
 @[simp] lemma map_zero [has_zero α] {β : Type w} [has_zero β] {f : α → β} (h : f 0 = 0) :
   (0 : matrix m n α).map f = 0 :=
@@ -100,14 +100,14 @@ variables [decidable_eq n]
 if `i ≠ j`. -/
 def diagonal [has_zero α] (d : n → α) : matrix n n α := λ i j, if i = j then d i else 0
 
-@[simp] theorem diagonal_val_eq [has_zero α] {d : n → α} (i : n) : (diagonal d) i i = d i :=
+@[simp] theorem diagonal_apply_eq [has_zero α] {d : n → α} (i : n) : (diagonal d) i i = d i :=
 by simp [diagonal]
 
-@[simp] theorem diagonal_val_ne [has_zero α] {d : n → α} {i j : n} (h : i ≠ j) :
+@[simp] theorem diagonal_apply_ne [has_zero α] {d : n → α} {i j : n} (h : i ≠ j) :
   (diagonal d) i j = 0 := by simp [diagonal, h]
 
-theorem diagonal_val_ne' [has_zero α] {d : n → α} {i j : n} (h : j ≠ i) :
-  (diagonal d) i j = 0 := diagonal_val_ne h.symm
+theorem diagonal_apply_ne' [has_zero α] {d : n → α} {i j : n} (h : j ≠ i) :
+  (diagonal d) i j = 0 := diagonal_apply_ne h.symm
 
 @[simp] theorem diagonal_zero [has_zero α] : (diagonal (λ _, 0) : matrix n n α) = 0 :=
 by simp [diagonal]; refl
@@ -118,7 +118,7 @@ begin
   ext i j,
   by_cases h : i = j,
   { simp [h, transpose] },
-  { simp [h, transpose, diagonal_val_ne' h] }
+  { simp [h, transpose, diagonal_apply_ne' h] }
 end
 
 @[simp] theorem diagonal_add [add_monoid α] (d₁ d₂ : n → α) :
@@ -137,43 +137,43 @@ instance : has_one (matrix n n α) := ⟨diagonal (λ _, 1)⟩
 
 @[simp] theorem diagonal_one : (diagonal (λ _, 1) : matrix n n α) = 1 := rfl
 
-theorem one_val {i j} : (1 : matrix n n α) i j = if i = j then 1 else 0 := rfl
+theorem one_apply {i j} : (1 : matrix n n α) i j = if i = j then 1 else 0 := rfl
 
-@[simp] theorem one_val_eq (i) : (1 : matrix n n α) i i = 1 := diagonal_val_eq i
+@[simp] theorem one_apply_eq (i) : (1 : matrix n n α) i i = 1 := diagonal_apply_eq i
 
-@[simp] theorem one_val_ne {i j} : i ≠ j → (1 : matrix n n α) i j = 0 :=
-diagonal_val_ne
+@[simp] theorem one_apply_ne {i j} : i ≠ j → (1 : matrix n n α) i j = 0 :=
+diagonal_apply_ne
 
-theorem one_val_ne' {i j} : j ≠ i → (1 : matrix n n α) i j = 0 :=
-diagonal_val_ne'
+theorem one_apply_ne' {i j} : j ≠ i → (1 : matrix n n α) i j = 0 :=
+diagonal_apply_ne'
 
 @[simp] lemma one_map {β : Type w} [has_zero β] [has_one β]
   {f : α → β} (h₀ : f 0 = 0) (h₁ : f 1 = 1) :
   (1 : matrix n n α).map f = (1 : matrix n n β) :=
-by { ext, simp only [one_val, map_apply], split_ifs; simp [h₀, h₁], }
+by { ext, simp only [one_apply, map_apply], split_ifs; simp [h₀, h₁], }
 
 end one
 
 section numeral
 
-@[simp] lemma bit0_val [has_add α] (M : matrix m m α) (i : m) (j : m) :
+@[simp] lemma bit0_apply [has_add α] (M : matrix m m α) (i : m) (j : m) :
   (bit0 M) i j = bit0 (M i j) := rfl
 
 variables [add_monoid α] [has_one α]
 
-lemma bit1_val (M : matrix n n α) (i : n) (j : n) :
+lemma bit1_apply (M : matrix n n α) (i : n) (j : n) :
   (bit1 M) i j = if i = j then bit1 (M i j) else bit0 (M i j) :=
 by dsimp [bit1]; by_cases h : i = j; simp [h]
 
 @[simp]
-lemma bit1_val_eq (M : matrix n n α) (i : n) :
+lemma bit1_apply_eq (M : matrix n n α) (i : n) :
   (bit1 M) i i = bit1 (M i i) :=
-by simp [bit1_val]
+by simp [bit1_apply]
 
 @[simp]
-lemma bit1_val_ne (M : matrix n n α) {i j : n} (h : i ≠ j) :
+lemma bit1_apply_ne (M : matrix n n α) {i j : n} (h : i ≠ j) :
   (bit1 M) i j = bit0 (M i j) :=
-by simp [bit1_val, h]
+by simp [bit1_apply, h]
 
 end numeral
 
@@ -219,17 +219,17 @@ by simp [dot_product, mul_add, finset.sum_add_distrib]
 
 @[simp] lemma diagonal_dot_product [decidable_eq m] [semiring α] (v w : m → α) (i : m) :
   dot_product (diagonal v i) w = v i * w i :=
-have ∀ j ≠ i, diagonal v i j * w j = 0 := λ j hij, by simp [diagonal_val_ne' hij],
+have ∀ j ≠ i, diagonal v i j * w j = 0 := λ j hij, by simp [diagonal_apply_ne' hij],
 by convert finset.sum_eq_single i (λ j _, this j) _; simp
 
 @[simp] lemma dot_product_diagonal [decidable_eq m] [semiring α] (v w : m → α) (i : m) :
   dot_product v (diagonal w i) = v i * w i :=
-have ∀ j ≠ i, v j * diagonal w i j = 0 := λ j hij, by simp [diagonal_val_ne' hij],
+have ∀ j ≠ i, v j * diagonal w i j = 0 := λ j hij, by simp [diagonal_apply_ne' hij],
 by convert finset.sum_eq_single i (λ j _, this j) _; simp
 
 @[simp] lemma dot_product_diagonal' [decidable_eq m] [semiring α] (v w : m → α) (i : m) :
   dot_product v (λ j, diagonal w j i) = v i * w i :=
-have ∀ j ≠ i, v j * diagonal w j i = 0 := λ j hij, by simp [diagonal_val_ne hij],
+have ∀ j ≠ i, v j * diagonal w j i = 0 := λ j hij, by simp [diagonal_apply_ne hij],
 by convert finset.sum_eq_single i (λ j _, this j) _; simp
 
 @[simp] lemma neg_dot_product [ring α] (v w : m → α) : dot_product (-v) w = - dot_product v w :=
@@ -254,15 +254,15 @@ protected def mul [has_mul α] [add_comm_monoid α] (M : matrix l m α) (N : mat
 
 localized "infixl ` ⬝ `:75 := matrix.mul" in matrix
 
-theorem mul_val [has_mul α] [add_comm_monoid α] {M : matrix l m α} {N : matrix m n α} {i k} :
+theorem mul_apply [has_mul α] [add_comm_monoid α] {M : matrix l m α} {N : matrix m n α} {i k} :
   (M ⬝ N) i k = ∑ j, M i j * N j k := rfl
 
 instance [has_mul α] [add_comm_monoid α] : has_mul (matrix n n α) := ⟨matrix.mul⟩
 
 @[simp] theorem mul_eq_mul [has_mul α] [add_comm_monoid α] (M N : matrix n n α) :
   M * N = M ⬝ N := rfl
 
-theorem mul_val' [has_mul α] [add_comm_monoid α] {M N : matrix n n α} {i k} :
+theorem mul_apply' [has_mul α] [add_comm_monoid α] {M N : matrix n n α} {i k} :
   (M ⬝ N) i k = dot_product (λ j, M i j) (λ j, N j k) := rfl
 
 section semigroup
@@ -334,7 +334,7 @@ diagonal_mul_diagonal _ _
 lemma map_mul {L : matrix m n α} {M : matrix n o α}
   {β : Type w} [semiring β] {f : α →+* β} :
 (L ⬝ M).map f = L.map f ⬝ M.map f :=
-by { ext, simp [mul_val, ring_hom.map_sum], }
+by { ext, simp [mul_apply, ring_hom.map_sum], }
 
 lemma is_add_monoid_hom_mul_left (M : matrix l m α) :
   is_add_monoid_hom (λ x : matrix m n α, M ⬝ x) :=
@@ -359,7 +359,7 @@ protected lemma mul_sum {β : Type*} (s : finset β) (f : β → matrix m n α)
   (id (@is_add_monoid_hom_mul_left _ _ n _ _ _ _ _ M) : _)).symm
 
 @[simp]
-lemma row_mul_col_val (v w : m → α) (i j) : (row v ⬝ col w) i j = dot_product v w :=
+lemma row_mul_col_apply (v w : m → α) (i j) : (row v ⬝ col w) i j = dot_product v w :=
 rfl
 
 end semiring
@@ -402,7 +402,7 @@ instance [semiring α] : has_scalar α (matrix m n α) := pi.has_scalar
 instance {β : Type w} [semiring α] [add_comm_monoid β] [semimodule α β] :
   semimodule α (matrix m n β) := pi.semimodule _ _ _
 
-@[simp] lemma smul_val [semiring α] (a : α) (A : matrix m n α) (i : m) (j : n) : (a • A) i j = a * A i j := rfl
+@[simp] lemma smul_apply [semiring α] (a : α) (A : matrix m n α) (i : m) (j : n) : (a • A) i j = a * A i j := rfl
 
 section semiring
 variables [semiring α]
@@ -417,7 +417,7 @@ by { ext, apply smul_dot_product }
 @[simp] lemma mul_mul_left (M : matrix m n α) (N : matrix n o α) (a : α) :
   (λ i j, a * M i j) ⬝ N = a • (M ⬝ N) :=
 begin
-  simp only [←smul_val],
+  simp only [←smul_apply],
   simp,
 end
 
@@ -440,11 +440,11 @@ variable [decidable_eq n]
 
 lemma scalar_apply_eq (a : α) (i : n) :
   scalar n a i i = a :=
-by simp only [coe_scalar, mul_one, one_val_eq, smul_val]
+by simp only [coe_scalar, mul_one, one_apply_eq, smul_apply]
 
 lemma scalar_apply_ne (a : α) (i j : n) (h : i ≠ j) :
   scalar n a i j = 0 :=
-by simp only [h, coe_scalar, one_val_ne, ne.def, not_false_iff, smul_val, mul_zero]
+by simp only [h, coe_scalar, one_apply_ne, ne.def, not_false_iff, smul_apply, mul_zero]
 
 end scalar
 
@@ -463,7 +463,7 @@ by { ext, apply dot_product_smul }
 @[simp] lemma mul_mul_right (M : matrix m n α) (N : matrix n o α) (a : α) :
   M ⬝ (λ i j, a * N i j) = a • (M ⬝ N) :=
 begin
-  simp only [←smul_val],
+  simp only [←smul_apply],
   simp,
 end
 
@@ -524,7 +524,7 @@ by { ext, symmetry, apply dot_product_assoc }
 
 lemma vec_mul_vec_eq (w : m → α) (v : n → α) :
   vec_mul_vec w v = (col w) ⬝ (row v) :=
-by { ext i j, simp [vec_mul_vec, mul_val], refl }
+by { ext i j, simp [vec_mul_vec, mul_apply], refl }
 
 variables [decidable_eq m] [decidable_eq n]
 
@@ -626,9 +626,9 @@ open_locale matrix
 /--
   Tell `simp` what the entries are in a transposed matrix.
 
-  Compare with `mul_val`, `diagonal_val_eq`, etc.
+  Compare with `mul_apply`, `diagonal_apply_eq`, etc.
 -/
-@[simp] lemma transpose_val (M : matrix m n α) (i j) : M.transpose j i = M i j := rfl
+@[simp] lemma transpose_apply (M : matrix m n α) (i j) : M.transpose j i = M i j := rfl
 
 @[simp] lemma transpose_transpose (M : matrix m n α) :
   Mᵀᵀ = M :=
@@ -642,8 +642,8 @@ begin
   ext i j,
   unfold has_one.one transpose,
   by_cases i = j,
-  { simp only [h, diagonal_val_eq] },
-  { simp only [diagonal_val_ne h, diagonal_val_ne (λ p, h (symm p))] }
+  { simp only [h, diagonal_apply_eq] },
+  { simp only [diagonal_apply_ne h, diagonal_apply_ne (λ p, h (symm p))] }
 end
 
 @[simp] lemma transpose_add [has_add α] (M : matrix m n α) (N : matrix m n α) :
@@ -726,8 +726,8 @@ open_locale matrix
 @[simp] lemma row_add [semiring α] (v w : m → α) : row (v + w) = row v + row w := by { ext, refl }
 @[simp] lemma row_smul [semiring α] (x : α) (v : m → α) : row (x • v) = x • row v := by { ext, refl }
 
-@[simp] lemma col_val (v : m → α) (i j) : matrix.col v i j = v i := rfl
-@[simp] lemma row_val (v : m → α) (i j) : matrix.row v i j = v j := rfl
+@[simp] lemma col_apply (v : m → α) (i j) : matrix.col v i j = v i := rfl
+@[simp] lemma row_apply (v : m → α) (i j) : matrix.row v i j = v j := rfl
 
 @[simp]
 lemma transpose_col (v : m → α) : (matrix.col v).transpose = matrix.row v := by {ext, refl}
@@ -769,15 +769,15 @@ function.update_same j (c i) (M i)
 @[simp] lemma update_column_ne [decidable_eq m] {j' : m} (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_val [decidable_eq n] {i' : n} :
+lemma update_row_apply [decidable_eq n] {i' : n} :
   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_val [decidable_eq m] {j' : m} : update_column M j c i j' = if j' = j then c i else M i j' :=
+lemma update_column_apply [decidable_eq m] {j' : m} : 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] },
@@ -787,14 +787,14 @@ end
 lemma update_row_transpose [decidable_eq m] : update_row Mᵀ j c = (update_column M j c)ᵀ :=
 begin
   ext i' j,
-  rw [transpose_val, update_row_val, update_column_val],
+  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)ᵀ :=
 begin
   ext i' j,
-  rw [transpose_val, update_row_val, update_column_val],
+  rw [transpose_apply, update_row_apply, update_column_apply],
   refl
 end
 
@@ -909,7 +909,8 @@ lemma from_blocks_multiply {p q : Type u} [fintype p] [fintype q]
               (C ⬝ A' + D ⬝ C') (C ⬝ B' + D ⬝ D') :=
 begin
   ext i j, rcases i; rcases j;
-  simp only [from_blocks, mul_val, fintype.sum_sum_type, sum.elim_inl, sum.elim_inr, pi.add_apply],
+  simp only [from_blocks, mul_apply, fintype.sum_sum_type, sum.elim_inl, sum.elim_inr,
+    pi.add_apply],
 end
 
 variables [decidable_eq l] [decidable_eq m]
@@ -921,7 +922,7 @@ begin
 end
 
 @[simp] lemma from_blocks_one : from_blocks (1 : matrix l l α) 0 0 (1 : matrix m m α) = 1 :=
-by { ext i j, rcases i; rcases j; simp [one_val] }
+by { ext i j, rcases i; rcases j; simp [one_apply] }
 
 end block_matrices
 
@@ -932,6 +933,6 @@ variables {β : Type*} [semiring α] [semiring β]
 
 lemma map_matrix_mul (M : matrix m n α) (N : matrix n o α) (i : m) (j : o) (f : α →+* β) :
   f (matrix.mul M N i j) = matrix.mul (λ i j, f (M i j)) (λ i j, f (N i j)) i j :=
-by simp [matrix.mul_val, ring_hom.map_sum]
+by simp [matrix.mul_apply, ring_hom.map_sum]
 
 end ring_hom

src/data/matrix/pequiv.lean

@@ -50,7 +50,7 @@ def to_matrix [decidable_eq n] [has_zero α] [has_one α] (f : m ≃. n) : matri
 lemma mul_matrix_apply [decidable_eq m] [semiring α] (f : l ≃. m) (M : matrix m n α) (i j) :
   (f.to_matrix ⬝ M) i j = option.cases_on (f i) 0 (λ fi, M fi j) :=
 begin
-  dsimp [to_matrix, matrix.mul_val],
+  dsimp [to_matrix, matrix.mul_apply],
   cases h : f i with fi,
   { simp [h] },
   { rw finset.sum_eq_single fi;
@@ -63,12 +63,12 @@ by ext; simp only [transpose, mem_iff_mem f, to_matrix]; congr
 
 @[simp] lemma to_matrix_refl [decidable_eq n] [has_zero α] [has_one α] :
   ((pequiv.refl n).to_matrix : matrix n n α) = 1 :=
-by ext; simp [to_matrix, one_val]; congr
+by ext; simp [to_matrix, one_apply]; congr
 
 lemma matrix_mul_apply [semiring α] [decidable_eq n] (M : matrix l m α) (f : m ≃. n) (i j) :
   (M ⬝ f.to_matrix) i j = option.cases_on (f.symm j) 0 (λ fj, M i fj) :=
 begin
-  dsimp [to_matrix, matrix.mul_val],
+  dsimp [to_matrix, matrix.mul_apply],
   cases h : f.symm j with fj,
   { simp [h, f.eq_some_iff.symm] },
   { conv in (_ ∈ _) { rw ← f.mem_iff_mem },
@@ -119,7 +119,7 @@ lemma to_matrix_swap [decidable_eq n] [ring α] (i j : n) :
     (single j i).to_matrix :=
 begin
   ext,
-  dsimp [to_matrix, single, equiv.swap_apply_def, equiv.to_pequiv, one_val],
+  dsimp [to_matrix, single, equiv.swap_apply_def, equiv.to_pequiv, one_apply],
   split_ifs; simp * at *
 end
 

src/linear_algebra/bilinear_form.lean

@@ -311,8 +311,8 @@ def matrix.to_bilin_formₗ : matrix n n R →ₗ[R] bilin_form R (n → R) :=
     bilin_smul_left := λ a x y, by simp,
     bilin_add_right := λ x y z, by simp [matrix.mul_add],
     bilin_smul_right := λ a x y, by simp },
-  map_add' := λ f g, by { ext, simp [add_apply, matrix.mul_add, matrix.add_mul] },
-  map_smul' := λ f g, by { ext, simp [smul_apply] } }
+  map_add' := λ f g, by { ext, simp [bilin_form.add_apply, matrix.mul_add, matrix.add_mul] },
+  map_smul' := λ f g, by { ext, simp [bilin_form.smul_apply] } }
 
 /-- The map from `matrix n n R` to bilinear forms on `n → R`. -/
 def matrix.to_bilin_form : matrix n n R → bilin_form R (n → R) :=
@@ -345,7 +345,7 @@ lemma bilin_form.to_matrix_comp (B : bilin_form R (n → R)) (l r : (o → R) 
   (B.comp l r).to_matrix = l.to_matrixᵀ ⬝ B.to_matrix ⬝ r.to_matrix :=
 begin
   ext i j,
-  simp only [to_matrix_apply, comp_apply, mul_val, sum_mul],
+  simp only [to_matrix_apply, comp_apply, mul_apply, sum_mul],
   have sum_smul_eq : Π (f : (o → R) →ₗ[R] (n → R)) (i : o),
     f (λ n, ite (n = i) 1 0) = ∑ k, f.to_matrix k i • λ n, ite (n = k) (1 : R) 0,
   { intros f i,
@@ -387,7 +387,7 @@ end
 
 @[simp] lemma to_bilin_form_to_matrix (M : matrix n n R) :
   M.to_bilin_form.to_matrix = M :=
-by { ext, simp [bilin_form.to_matrix_apply, matrix.to_bilin_form_apply, mul_val], }
+by { ext, simp [bilin_form.to_matrix_apply, matrix.to_bilin_form_apply, mul_apply], }
 
 /-- Bilinear forms are linearly equivalent to matrices. -/
 def bilin_form_equiv_matrix : bilin_form R (n → R) ≃ₗ[R] matrix n n R :=

src/linear_algebra/char_poly/coeff.lean

@@ -140,7 +140,7 @@ begin
   { unfold finsupp.sum, rw sum_apply, rw sum_apply, dsimp, refl, },
   { simp_rw ← (scalar n).map_pow, simp_rw ← (matrix.scalar.commute _ _).eq,
     simp only [coe_scalar, matrix.one_mul, ring_hom.id_apply,
-      smul_val, mul_eq_mul, algebra.smul_mul_assoc],
+      smul_apply, mul_eq_mul, algebra.smul_mul_assoc],
     have h : ∀ x : ℕ, (λ (e : ℕ) (a : R), r ^ e * a) x 0 = 0 := by simp,
     symmetry, rw ← finsupp.sum_map_range_index h, swap, refl,
     refine congr (congr rfl _) (by {ext, rw mul_comm}), ext, rw finsupp.map_range_apply,