[Merged by Bors] - feat(data/matrix/basic): miscellaneous defs and lemmas

src/data/matrix/basic.lean

@@ -1,4 +1,4 @@
 /-
 Copyright (c) 2018 Ellen Arlt. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ellen Arlt, Blair Shi, Sean Leather, Mario Carneiro, Johan Commelin, Lu-Ming Zhang
@@ -472,6 +472,14 @@
   v ⬝ᵥ w = v ⟨⟩ * w ⟨⟩ :=
 by simp [dot_product]
 
+section mul_one_class
+variables [mul_one_class α] [add_comm_monoid α]
+
+lemma dot_product_one (v : n → α) : v ⬝ᵥ 1 = ∑ i, v i := by simp [(⬝ᵥ)]
+lemma one_dot_product (v : n → α) : 1 ⬝ᵥ v = ∑ i, v i := by simp [(⬝ᵥ)]
+
+end mul_one_class
+
 section non_unital_non_assoc_semiring
 variables [non_unital_non_assoc_semiring α] (u v w : m → α) (x y : n → α)
 
@@ -533,6 +541,14 @@
 
 end non_unital_non_assoc_semiring_decidable
 
+section non_assoc_semiring
+variables [non_assoc_semiring α]
+
+@[simp] lemma one_dot_product_one : (1 : n → α) ⬝ᵥ 1 = fintype.card n :=
+by simp [dot_product, fintype.card]
+
+end non_assoc_semiring
+
 section non_unital_non_assoc_ring
 variables [non_unital_non_assoc_ring α] (u v w : m → α)
 
@@ -1305,7 +1321,15 @@
 end non_unital_semiring
 
 section non_assoc_semiring
-variables [fintype m] [decidable_eq m] [non_assoc_semiring α]
+variables [non_assoc_semiring α]
+
+lemma mul_vec_one [fintype n] (A : matrix m n α) : mul_vec A 1 = λ i, ∑ j, A i j :=
+by ext; simp [mul_vec, dot_product]
+
+lemma vec_one_mul [fintype m] (A : matrix m n α) : vec_mul 1 A = λ j, ∑ i, A i j :=
+by ext; simp [vec_mul, dot_product]
+
+variables [fintype m] [fintype n] [decidable_eq m]
 
 @[simp] lemma one_mul_vec (v : m → α) : mul_vec 1 v = v :=
 by { ext, rw [←diagonal_one, mul_vec_diagonal, one_mul] }
@@ -1816,10 +1840,11 @@
   vec_mul v (M.submatrix e₁ e₂) = vec_mul (v ∘ e₁.symm) M ∘ e₂ :=
 funext $ λ i, eq.symm (comp_equiv_symm_dot_product _ _ _)
 
-lemma mul_submatrix_one [fintype n] [fintype o] [non_assoc_semiring α] [decidable_eq o] (e₁ : n ≃ o)
+lemma mul_submatrix_one [fintype n] [finite o] [non_assoc_semiring α] [decidable_eq o] (e₁ : n ≃ o)
   (e₂ : l → o) (M : matrix m n α) :
   M ⬝ (1 : matrix o o α).submatrix e₁ e₂ = submatrix M id (e₁.symm ∘ e₂) :=
 begin
+  casesI nonempty_fintype o,
   let A := M.submatrix id e₁.symm,
   have : M = A.submatrix id e₁,
   { simp only [submatrix_submatrix, function.comp.right_id, submatrix_id_id,
@@ -1829,10 +1854,11 @@
     equiv.symm_comp_self],
 end
 
-lemma one_submatrix_mul [fintype m] [fintype o] [non_assoc_semiring α] [decidable_eq o] (e₁ : l → o)
+lemma one_submatrix_mul [fintype m] [finite o] [non_assoc_semiring α] [decidable_eq o] (e₁ : l → o)
   (e₂ : m ≃ o) (M : matrix m n α) :
   ((1 : matrix o o α).submatrix e₁ e₂).mul M = submatrix M (e₂.symm ∘ e₁) id :=
 begin
+  casesI nonempty_fintype o,
   let A := M.submatrix e₂.symm id,
   have : M = A.submatrix e₂ id,
   { simp only [submatrix_submatrix, function.comp.right_id, submatrix_id_id,

src/data/matrix/block.lean

@@ -1,4 +1,4 @@
 /-
 Copyright (c) 2018 Ellen Arlt. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ellen Arlt, Blair Shi, Sean Leather, Mario Carneiro, Johan Commelin
@@ -27,10 +27,14 @@
 variables {l m n o p q : Type*} {m' n' p' : o → Type*}
 variables {R : Type*} {S : Type*} {α : Type*} {β : Type*}
 
-open_locale matrix
+open_locale big_operators matrix
 
 namespace matrix
 
+lemma dot_product_block [fintype m] [fintype n] [has_mul α] [add_comm_monoid α] (v w : m ⊕ n → α) :
+  v ⬝ᵥ w = v ∘ sum.inl ⬝ᵥ w ∘ sum.inl + v ∘ sum.inr ⬝ᵥ w ∘ sum.inr :=
+fintype.sum_sum_type _
+
 section block_matrices
 
 /-- We can form a single large matrix by flattening smaller 'block' matrices of compatible