[Merged by Bors] - chore(data/matrix/basic): clean up of new lemmas on matrix numerals

src/data/matrix/basic.lean

@@ -100,15 +100,32 @@ theorem one_val_ne' {i j} : j ≠ i → (1 : matrix n n α) i j = 0 :=
 diagonal_val_ne'
 
 end one
+
 end diagonal
 
-@[simp] lemma bit0_apply_apply [has_add α] (M : matrix n n α) (i : n) (j : n) :
+section numeral
+
+@[simp] lemma bit0_val [has_add α] (M : matrix n n α) (i : n) (j : n) :
   (bit0 M) i j = bit0 (M i j) := rfl
 
-@[simp] lemma bit1_apply_apply [decidable_eq n] [semiring α] (M : matrix n n α) (i : n) (j : n) :
+variables [decidable_eq n] [add_monoid α] [has_one α]
+
+lemma bit1_val (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 i = j; simp [h]
 
+@[simp]
+lemma bit1_val_eq (M : matrix n n α) (i : n) :
+  (bit1 M) i i = bit1 (M i i) :=
+by simp [bit1_val]
+
+@[simp]
+lemma bit1_val_ne (M : matrix n n α) {i j : n} (h : i ≠ j) :
+  (bit1 M) i j = bit0 (M i j) :=
+by simp [bit1_val, h]
+
+end numeral
+
 @[simp] theorem diagonal_add [decidable_eq n] [add_monoid α] (d₁ d₂ : n → α) :
   diagonal d₁ + diagonal d₂ = diagonal (λ i, d₁ i + d₂ i) :=
 by ext i j; by_cases i = j; simp [h]