From 6c65a6ea4ad602c3a79ef98a1bb74f7469e1f2a9 Mon Sep 17 00:00:00 2001 From: l534zhan Date: Tue, 13 Jul 2021 11:57:32 +0100 Subject: [PATCH 01/29] miscellaneous defs and lemmas --- src/data/matrix/basic.lean | 218 ++++++++++++++++++++++++++++-------- src/data/matrix/pequiv.lean | 7 ++ 2 files changed, 179 insertions(+), 46 deletions(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index 03fc7ae27402e..e057f1a9c4190 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -1,7 +1,7 @@ /- 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 +Authors: Ellen Arlt, Blair Shi, Sean Leather, Mario Carneiro, Johan Commelin, Lu-Ming Zhang -/ import algebra.big_operators.pi import algebra.module.pi @@ -26,24 +26,120 @@ open dmatrix def matrix (m : Type u) (n : Type u') [fintype m] [fintype n] (α : Type v) : Type (max u u' v) := m → n → α -variables {l m n o : Type*} [fintype l] [fintype m] [fintype n] [fintype o] +variables {l m n o p q: Type*} [fintype l] +variables [fintype m] [fintype n] [fintype o] [fintype p] [fintype q] variables {m' : o → Type*} [∀ i, fintype (m' i)] variables {n' : o → Type*} [∀ i, fintype (n' i)] variables {R : Type*} {S : Type*} {α : Type v} {β : Type w} +/-- `equiv.perm.to_matrix` converts a permutation `σ : equiv.perm m` to a matrix + containing ones and zeros. This definition is then used to define the Prop `matrix.is_perm`. + `equiv.perm.to_prequiv_to_matrix_eq_to_matrix` proves that + `σ.to_pequiv.to_matrix = σ.to_matrix` in `pequiv.lean`.-/ +def equiv.perm.to_matrix [decidable_eq m] [has_zero α] [has_one α] (σ : equiv.perm m) : +matrix m m α +| i j := if σ i = j then 1 else 0 + namespace matrix +instance [inhabited α] : inhabited (matrix m n α) := pi.inhabited _ +instance [has_add α] : has_add (matrix m n α) := pi.has_add +instance [add_semigroup α] : add_semigroup (matrix m n α) := pi.add_semigroup +instance [add_comm_semigroup α] : add_comm_semigroup (matrix m n α) := pi.add_comm_semigroup +instance [has_zero α] : has_zero (matrix m n α) := pi.has_zero +instance [add_monoid α] : add_monoid (matrix m n α) := pi.add_monoid +instance [add_comm_monoid α] : add_comm_monoid (matrix m n α) := pi.add_comm_monoid +instance [has_neg α] : has_neg (matrix m n α) := pi.has_neg +instance [has_sub α] : has_sub (matrix m n α) := pi.has_sub +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 +instance [unique α] : unique (matrix m n α) := pi.unique +instance [subsingleton α] : subsingleton (matrix m n α) := pi.subsingleton +instance [nonempty m] [nonempty n] [nontrivial α] : nontrivial (matrix m n α) := +function.nontrivial + +instance [has_scalar R α] : has_scalar R (matrix m n α) := pi.has_scalar +instance [has_scalar R α] [has_scalar S α] [smul_comm_class R S α] : + smul_comm_class R S (matrix m n α) := pi.smul_comm_class +instance [has_scalar R S] [has_scalar R α] [has_scalar S α] [is_scalar_tower R S α] : + is_scalar_tower R S (matrix m n α) := pi.is_scalar_tower +instance [monoid R] [mul_action R α] : + mul_action R (matrix m n α) := pi.mul_action _ +instance [monoid R] [add_monoid α] [distrib_mul_action R α] : + distrib_mul_action R (matrix m n α) := pi.distrib_mul_action _ +instance [semiring R] [add_comm_monoid α] [module R α] : + module R (matrix m n α) := pi.module _ _ _ + section ext + variables {M N : matrix m n α} theorem ext_iff : (∀ i j, M i j = N i j) ↔ M = N := ⟨λ h, funext $ λ i, funext $ h i, λ h, by simp [h]⟩ -@[ext] theorem ext : (∀ i j, M i j = N i j) → M = N := -ext_iff.mp +@[ext] theorem ext : (∀ i j, M i j = N i j) → M = N := ext_iff.mp end ext +section transpose + +/-- The transpose of a matrix. -/ +def transpose (M : matrix m n α) : matrix n m α +| x y := M y x +localized "postfix `ᵀ`:1500 := matrix.transpose" in matrix + +lemma trans_col_eq_row (A : matrix m n α) (i : m) : (λ j, Aᵀ j i) = A i := +by simp [transpose] +lemma trans_row_eq_col (A : matrix m n α) (j : n) : Aᵀ j = (λ i, A i j):= +by ext; simp [transpose] + +instance vec_has_star [has_star α]: has_star (n → α) := ⟨λ v i, star (v i)⟩ +@[simp] lemma vec_star_ext [has_star α] (v : n → α) (i : n) : star v i = star (v i) := rfl + +def conj_transpose [has_star α] (M : matrix m n α) : matrix n m α +| x y := star (M y x) +localized "postfix `ᴴ`:1500 := matrix.conj_transpose" in matrix + +end transpose + +open_locale matrix + +protected def is_sym (A : matrix m m α) : Prop := Aᵀ = A + +protected def is_skewsym [has_neg α] (A : matrix m m α) : Prop := -Aᵀ = A + +protected def is_Hermitian [has_star α] (A : matrix m m α) : Prop := Aᴴ = A + +/-- Proposition `matrix.is_perm`. + `P.is_perm` means `P` is a permutation matrix. + A new file is probably required for systematically investigating permutation matrices. -/ +protected def is_perm [decidable_eq m] [has_zero α] [has_one α] (P : matrix m m α): Prop := +∃ σ : equiv.perm m, P = equiv.perm.to_matrix σ + +/-- Proposition `matrix.is_perfect_shuffle`. + `P.is_perfect_shuffle` means `P` is a perfect shuffle matrix. + A new file is probably required for systematically investigating perfect shuffle matrices. -/ +protected def is_perfect_shuffle +[decidable_eq m] [has_zero α] [has_one α] (P : matrix m m α) : Prop := +∃ σ : equiv.perm m, (P = equiv.perm.to_matrix σ ∧ ∀ i : m, σ i ≠ i) + +/-- The "trace" of a matrix. + A different version of "trace" is defined in `trace.lean` as `matrix.trace`. + One advantage of `matrix.tr` is that this definition is more elementary, + which only requires α to be a `add_comm_monoid`; whilst `matrix.trace` requires + `[semiring β] [add_comm_monoid α] [module β α]`. + The equivalence can be easily established when `α` is indeed a `β-module`. + Another advantage is that `matrix.tr` is more convenient for users to explore lemmas/theorems + involving "tace" from a combinatorial aspect.-/ +def tr [add_comm_monoid α] (A : matrix n n α) : α := ∑ i : n, A i i +/- +lemma trace_eq_tr [semiring β] [add_comm_monoid α] [module β α] (A : matrix n n α) +: trace n β α A = tr A := rfl +-/ + +lemma eq_of_empty [c: is_empty m] (M N: matrix m m α) : M = N := +by {ext, exfalso, apply is_empty_iff.mp c i} + /-- `M.map f` is the matrix obtained by applying `f` to each entry of the matrix `M`. -/ def map (M : matrix m n α) (f : α → β) : matrix m n β := λ i j, f (M i j) @@ -56,12 +152,6 @@ lemma map_map {M : matrix m n α} {β γ : Type*} {f : α → β} {g : β → γ (M.map f).map g = M.map (g ∘ f) := by { ext, simp, } -/-- The transpose of a matrix. -/ -def transpose (M : matrix m n α) : matrix n m α -| x y := M y x - -localized "postfix `ᵀ`:1500 := matrix.transpose" in matrix - /-- `matrix.col u` is the column matrix whose entries are given by `u`. -/ def col (w : m → α) : matrix m unit α | x y := w x @@ -70,34 +160,6 @@ def col (w : m → α) : matrix m unit α def row (v : n → α) : matrix unit n α | x y := v y -instance [inhabited α] : inhabited (matrix m n α) := pi.inhabited _ -instance [has_add α] : has_add (matrix m n α) := pi.has_add -instance [add_semigroup α] : add_semigroup (matrix m n α) := pi.add_semigroup -instance [add_comm_semigroup α] : add_comm_semigroup (matrix m n α) := pi.add_comm_semigroup -instance [has_zero α] : has_zero (matrix m n α) := pi.has_zero -instance [add_monoid α] : add_monoid (matrix m n α) := pi.add_monoid -instance [add_comm_monoid α] : add_comm_monoid (matrix m n α) := pi.add_comm_monoid -instance [has_neg α] : has_neg (matrix m n α) := pi.has_neg -instance [has_sub α] : has_sub (matrix m n α) := pi.has_sub -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 -instance [unique α] : unique (matrix m n α) := pi.unique -instance [subsingleton α] : subsingleton (matrix m n α) := pi.subsingleton -instance [nonempty m] [nonempty n] [nontrivial α] : nontrivial (matrix m n α) := -function.nontrivial - -instance [has_scalar R α] : has_scalar R (matrix m n α) := pi.has_scalar -instance [has_scalar R α] [has_scalar S α] [smul_comm_class R S α] : - smul_comm_class R S (matrix m n α) := pi.smul_comm_class -instance [has_scalar R S] [has_scalar R α] [has_scalar S α] [is_scalar_tower R S α] : - is_scalar_tower R S (matrix m n α) := pi.is_scalar_tower -instance [monoid R] [mul_action R α] : - mul_action R (matrix m n α) := pi.mul_action _ -instance [monoid R] [add_monoid α] [distrib_mul_action R α] : - distrib_mul_action R (matrix m n α) := pi.distrib_mul_action _ -instance [semiring R] [add_comm_monoid α] [module R α] : - module R (matrix m n α) := pi.module _ _ _ - @[simp] lemma map_zero [has_zero α] [has_zero β] {f : α → β} (h : f 0 = 0) : (0 : matrix m n α).map f = 0 := by { ext, simp [h], } @@ -251,22 +313,50 @@ by simp_rw [dot_product, mul_comm] dot_product v w = v ⟨⟩ * w ⟨⟩ := by simp [dot_product] -@[simp] lemma dot_product_zero [non_unital_non_assoc_semiring α] (v : m → α) : - dot_product v 0 = 0 := +section dot_product_zero + +variables [non_unital_non_assoc_semiring α] (v : m → α) + +@[simp] lemma dot_product_zero : dot_product v 0 = 0 := by simp [dot_product] -@[simp] lemma dot_product_zero' [non_unital_non_assoc_semiring α] (v : m → α) : - dot_product v (λ _, 0) = 0 := +@[simp] lemma dot_product_zero' : dot_product v (λ _, 0) = 0 := dot_product_zero v -@[simp] lemma zero_dot_product [non_unital_non_assoc_semiring α] (v : m → α) : - dot_product 0 v = 0 := +@[simp] lemma zero_dot_product : dot_product 0 v = 0 := by simp [dot_product] -@[simp] lemma zero_dot_product' [non_unital_non_assoc_semiring α] (v : m → α) : - dot_product (λ _, (0 : α)) v = 0 := +@[simp] lemma zero_dot_product' : dot_product (λ _, (0 : α)) v = 0 := zero_dot_product v +end dot_product_zero + +section dot_product_one + +def vec_one [has_one α] : n → α := λ x, 1 + +variables [mul_one_class α] [add_comm_monoid α] + +@[simp] lemma dot_product_one (v : n → α) : dot_product v vec_one = ∑ i, v i := +by simp [dot_product, vec_one] + +@[simp] lemma dot_product_one' (v : n → α) : dot_product v (λ i, 1) = ∑ i, v i := +by simp [dot_product] + +@[simp] lemma one_dot_product (v : n → α) : dot_product vec_one v = ∑ i, v i := +by simp [dot_product, vec_one] + +@[simp] lemma one_dot_product' (v : n → α) : dot_product (λ i, 1 : n → α) v = ∑ i, v i := +by simp [dot_product] + +lemma one_dot_one_eq_card : dot_product (vec_one : n → α) vec_one = fintype.card n := +by simp [dot_product, vec_one, fintype.card] + +lemma one_dot_one_eq_card' : dot_product (λ i, 1 : n → α) (λ i, 1) = fintype.card n := +by simp [dot_product, fintype.card] + +end dot_product_one + @[simp] lemma add_dot_product [non_unital_non_assoc_semiring α] (u v w : m → α) : dot_product (u + v) w = dot_product u w + dot_product v w := by simp [dot_product, add_mul, finset.sum_add_distrib] @@ -275,6 +365,14 @@ by simp [dot_product, add_mul, finset.sum_add_distrib] dot_product u (v + w) = dot_product u v + dot_product u w := by simp [dot_product, mul_add, finset.sum_add_distrib] +lemma dot_product_block' [has_mul α] [add_comm_monoid α] (v w : m ⊕ n → α) : +dot_product v w = ∑ i, v (sum.inl i) * w (sum.inl i) + ∑ j, v (sum.inr j) * w (sum.inr j) := +by {rw [dot_product, ←fintype.sum_sum_elim], congr, ext (i | j); simp } + +lemma dot_product_block [has_mul α] [add_comm_monoid α] (v w : m ⊕ n → α) : +dot_product v w = dot_product (λ i, v (sum.inl i)) (λ i, w (sum.inl i)) + dot_product (λ j, v (sum.inr j)) (λ j, w (sum.inr j)) := +by simp [dot_product, dot_product_block'] + @[simp] lemma diagonal_dot_product [decidable_eq m] [non_unital_non_assoc_semiring α] (v w : m → α) (i : m) : dot_product (diagonal v i) w = v i * w i := @@ -710,6 +808,18 @@ by { ext, rw [←diagonal_one, mul_vec_diagonal, one_mul] } @[simp] lemma vec_mul_one [decidable_eq m] (v : m → α) : vec_mul v 1 = v := by { ext, rw [←diagonal_one, vec_mul_diagonal, mul_one] } +@[simp] lemma mul_vector_one (A : matrix m n α) : mul_vec A vec_one = λ i, ∑ j, A i j := +by ext; simp [mul_vec, vec_one, dot_product] + +@[simp] lemma mul_vector_one' (A : matrix m n α) : mul_vec A (λ i, 1) = λ i, ∑ j, A i j := +by ext; simp [mul_vec, dot_product] + +@[simp] lemma vector_one_mul (A : matrix m n α) : vec_mul vec_one A = λ j, ∑ i, A i j := +by ext; simp [vec_mul, vec_one, dot_product] + +@[simp] lemma vector_one_mul' (A : matrix m n α) : vec_mul (λ j, 1 : m → α) A = λ j, ∑ i, A i j := +by ext; simp [vec_mul, dot_product] + end non_assoc_semiring section semiring @@ -895,6 +1005,10 @@ instance : star_ring (matrix n n α) := lemma star_mul (M N : matrix n n α) : star (M ⬝ N) = star N ⬝ star M := star_mul _ _ +lemma conj_transpose_eq_star_of_square_matrix +[decidable_eq m] [semiring α] [star_ring α] (M : matrix m m α) : +Mᴴ = star M := rfl + end star_ring /-- Given maps `(r_reindex : l → m)` and `(c_reindex : o → n)` reindexing the rows and columns of @@ -1024,6 +1138,18 @@ def reindex (eₘ : m ≃ l) (eₙ : n ≃ o) : matrix m n α ≃ matrix l o α left_inv := λ M, by simp, right_inv := λ M, by simp, } +def reindex_prod_assoc : matrix ((l × m) × n) ((o × p) × q) α ≃ matrix (l × m × n) (o × p × q) α := +reindex (equiv.prod_assoc _ _ _) (equiv.prod_assoc _ _ _) + +def reindex_prod_comm_snd : matrix l (m × n) α ≃ matrix l (n × m) α := +reindex (equiv.refl _) (equiv.prod_comm _ _) + +def reindex_prod_comm_fst : matrix (l × m) n α ≃ matrix (m × l) n α := +reindex (equiv.prod_comm _ _) (equiv.refl _) + +def reindex_prod_comm : matrix (m × n) (p × q) α ≃ matrix (n × m) (q × p) α := +reindex (equiv.prod_comm _ _) (equiv.prod_comm _ _) + @[simp] lemma reindex_apply (eₘ : m ≃ l) (eₙ : n ≃ o) (M : matrix m n α) : reindex eₘ eₙ M = M.minor eₘ.symm eₙ.symm := rfl diff --git a/src/data/matrix/pequiv.lean b/src/data/matrix/pequiv.lean index 4ff339d17176f..89c404d4b172f 100644 --- a/src/data/matrix/pequiv.lean +++ b/src/data/matrix/pequiv.lean @@ -48,6 +48,13 @@ open_locale matrix def to_matrix [decidable_eq n] [has_zero α] [has_one α] (f : m ≃. n) : matrix m n α | i j := if j ∈ f i then 1 else 0 +/-- `equiv.perm.to_prequiv_to_matrix_eq_to_matrix` proves that + `σ.to_pequiv.to_matrix = σ.to_matrix` for a permutation `σ : equiv.perm m`.-/ +lemma _root_.equiv.perm.to_prequiv_to_matrix_eq_to_matrix +[decidable_eq n] [has_zero α] [has_one α] (σ : equiv.perm n) : +(σ.to_pequiv.to_matrix : matrix n n α)= σ.to_matrix := +by ext i j; simp [pequiv.to_matrix, equiv.perm.to_matrix,equiv.to_pequiv] + 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 From 3ca697c25a4e01a51dac5dfa2103bb83a42c4abd Mon Sep 17 00:00:00 2001 From: l534zhan Date: Tue, 13 Jul 2021 13:20:22 +0100 Subject: [PATCH 02/29] fixed typos --- src/data/matrix/basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index e057f1a9c4190..f2b631931a075 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -130,7 +130,7 @@ protected def is_perfect_shuffle `[semiring β] [add_comm_monoid α] [module β α]`. The equivalence can be easily established when `α` is indeed a `β-module`. Another advantage is that `matrix.tr` is more convenient for users to explore lemmas/theorems - involving "tace" from a combinatorial aspect.-/ + involving "trace" from a combinatorial aspect.-/ def tr [add_comm_monoid α] (A : matrix n n α) : α := ∑ i : n, A i i /- lemma trace_eq_tr [semiring β] [add_comm_monoid α] [module β α] (A : matrix n n α) @@ -333,7 +333,7 @@ end dot_product_zero section dot_product_one -def vec_one [has_one α] : n → α := λ x, 1 +def vec_one [has_one α] : n → α := 1 variables [mul_one_class α] [add_comm_monoid α] From 5f586369610a9b220cdfe9886ca17933d26cf4e5 Mon Sep 17 00:00:00 2001 From: l534zhan Date: Tue, 13 Jul 2021 13:40:54 +0100 Subject: [PATCH 03/29] fixed typos --- src/data/matrix/basic.lean | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index f2b631931a075..3066c77916897 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -988,6 +988,13 @@ by { ext, refl } end transpose +section has_star +variables [has_star α] +instance : has_star (matrix n n α) := {star := conj_transpose} +lemma conj_transpose_eq_star_of_square_matrix (M : matrix m m α) : +star M = Mᴴ := rfl +end has_star + section star_ring variables [decidable_eq n] [semiring α] [star_ring α] @@ -1005,10 +1012,6 @@ instance : star_ring (matrix n n α) := lemma star_mul (M N : matrix n n α) : star (M ⬝ N) = star N ⬝ star M := star_mul _ _ -lemma conj_transpose_eq_star_of_square_matrix -[decidable_eq m] [semiring α] [star_ring α] (M : matrix m m α) : -Mᴴ = star M := rfl - end star_ring /-- Given maps `(r_reindex : l → m)` and `(c_reindex : o → n)` reindexing the rows and columns of From 7e7684ab109ae691cb249a42be0ab4ca907366f1 Mon Sep 17 00:00:00 2001 From: l534zhan Date: Tue, 13 Jul 2021 13:48:44 +0100 Subject: [PATCH 04/29] fixed things --- src/data/matrix/basic.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index 3066c77916897..a66be1b0ebde4 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -370,7 +370,9 @@ dot_product v w = ∑ i, v (sum.inl i) * w (sum.inl i) + ∑ j, v (sum.inr j) * by {rw [dot_product, ←fintype.sum_sum_elim], congr, ext (i | j); simp } lemma dot_product_block [has_mul α] [add_comm_monoid α] (v w : m ⊕ n → α) : -dot_product v w = dot_product (λ i, v (sum.inl i)) (λ i, w (sum.inl i)) + dot_product (λ j, v (sum.inr j)) (λ j, w (sum.inr j)) := +dot_product v w = +dot_product (λ i, v (sum.inl i)) (λ i, w (sum.inl i)) + +dot_product (λ j, v (sum.inr j)) (λ j, w (sum.inr j)) := by simp [dot_product, dot_product_block'] @[simp] lemma diagonal_dot_product [decidable_eq m] [non_unital_non_assoc_semiring α] @@ -1141,7 +1143,8 @@ def reindex (eₘ : m ≃ l) (eₙ : n ≃ o) : matrix m n α ≃ matrix l o α left_inv := λ M, by simp, right_inv := λ M, by simp, } -def reindex_prod_assoc : matrix ((l × m) × n) ((o × p) × q) α ≃ matrix (l × m × n) (o × p × q) α := +def reindex_prod_assoc : +matrix ((l × m) × n) ((o × p) × q) α ≃ matrix (l × m × n) (o × p × q) α := reindex (equiv.prod_assoc _ _ _) (equiv.prod_assoc _ _ _) def reindex_prod_comm_snd : matrix l (m × n) α ≃ matrix l (n × m) α := From 5594f808d3d73d2862731cdd0fcfaba367152c73 Mon Sep 17 00:00:00 2001 From: l534zhan Date: Wed, 14 Jul 2021 11:40:45 +0100 Subject: [PATCH 05/29] change --- src/data/matrix/basic.lean | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index a66be1b0ebde4..eba7a4a5a0c12 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -93,9 +93,6 @@ by simp [transpose] lemma trans_row_eq_col (A : matrix m n α) (j : n) : Aᵀ j = (λ i, A i j):= by ext; simp [transpose] -instance vec_has_star [has_star α]: has_star (n → α) := ⟨λ v i, star (v i)⟩ -@[simp] lemma vec_star_ext [has_star α] (v : n → α) (i : n) : star v i = star (v i) := rfl - def conj_transpose [has_star α] (M : matrix m n α) : matrix n m α | x y := star (M y x) localized "postfix `ᴴ`:1500 := matrix.conj_transpose" in matrix @@ -1010,8 +1007,6 @@ instance : star_ring (matrix n n α) := star_add := λ M N, by { ext, simp, }, star_mul := λ M N, by { ext, simp [mul_apply], }, } -@[simp] lemma star_apply (M : matrix n n α) (i j) : star M i j = star (M j i) := rfl - lemma star_mul (M N : matrix n n α) : star (M ⬝ N) = star N ⬝ star M := star_mul _ _ end star_ring From 53920175957fc470b097de66c26761e71f10d594 Mon Sep 17 00:00:00 2001 From: l534zhan Date: Wed, 14 Jul 2021 13:02:18 +0100 Subject: [PATCH 06/29] change --- src/data/matrix/basic.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index 34cdc276d95bd..551937207f09d 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -26,8 +26,7 @@ open dmatrix def matrix (m : Type u) (n : Type u') [fintype m] [fintype n] (α : Type v) : Type (max u u' v) := m → n → α -variables {l m n o p q: Type*} [fintype l] -variables [fintype m] [fintype n] [fintype o] [fintype p] [fintype q] +variables {l m n o: Type*} [fintype l] [fintype m] [fintype n] [fintype o] variables {m' : o → Type*} [∀ i, fintype (m' i)] variables {n' : o → Type*} [∀ i, fintype (n' i)] variables {R : Type*} {S : Type*} {α : Type v} {β : Type w} From 0d40ddc117e21f4fd9540184f6e667d583e506e2 Mon Sep 17 00:00:00 2001 From: l534zhan Date: Wed, 14 Jul 2021 13:10:29 +0100 Subject: [PATCH 07/29] change --- src/data/matrix/basic.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index 551937207f09d..c886a015a36f1 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -80,9 +80,6 @@ theorem ext_iff : (∀ i j, M i j = N i j) ↔ M = N := end ext -lemma eq_of_empty [c: is_empty m] (M N: matrix m m α) : M = N := -by {ext, exfalso, apply is_empty_iff.mp c i} - /-- `M.map f` is the matrix obtained by applying `f` to each entry of the matrix `M`. -/ def map (M : matrix m n α) (f : α → β) : matrix m n β := λ i j, f (M i j) @@ -161,6 +158,11 @@ lemma subsingleton_of_empty_left [is_empty m] : subsingleton (matrix m n α) := lemma subsingleton_of_empty_right [is_empty n] : subsingleton (matrix m n α) := ⟨λ M N, by { ext, exact is_empty_elim j }⟩ +local attribute [instance] matrix.subsingleton_of_empty_left matrix.subsingleton_of_empty_right + +lemma eq_of_empty [c: is_empty m] (M N: matrix m m α) : M = N := +subsingleton.elim M N + end matrix /-- The `add_monoid_hom` between spaces of matrices induced by an `add_monoid_hom` between their From a1afb10c8a529732b71573e73f771967c8707d42 Mon Sep 17 00:00:00 2001 From: l534zhan Date: Wed, 14 Jul 2021 13:40:30 +0100 Subject: [PATCH 08/29] typo --- src/data/matrix/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index c886a015a36f1..462a1c88d0149 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -26,7 +26,7 @@ open dmatrix def matrix (m : Type u) (n : Type u') [fintype m] [fintype n] (α : Type v) : Type (max u u' v) := m → n → α -variables {l m n o: Type*} [fintype l] [fintype m] [fintype n] [fintype o] +variables {l m n o : Type*} [fintype l] [fintype m] [fintype n] [fintype o] variables {m' : o → Type*} [∀ i, fintype (m' i)] variables {n' : o → Type*} [∀ i, fintype (n' i)] variables {R : Type*} {S : Type*} {α : Type v} {β : Type w} From accea2e49c95e726b157919f3dc4b2c59d2959bd Mon Sep 17 00:00:00 2001 From: l534zhan Date: Wed, 14 Jul 2021 16:02:57 +0100 Subject: [PATCH 09/29] --- src/data/matrix/basic.lean | 5 ++++- src/linear_algebra/matrix/nonsingular_inverse.lean | 2 +- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index 462a1c88d0149..0a4a77aaba6df 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -160,7 +160,10 @@ lemma subsingleton_of_empty_right [is_empty n] : subsingleton (matrix m n α) := local attribute [instance] matrix.subsingleton_of_empty_left matrix.subsingleton_of_empty_right -lemma eq_of_empty [c: is_empty m] (M N: matrix m m α) : M = N := +lemma empty_eq_empty_left [is_empty m] (M N: matrix m n α) : M = N := +subsingleton.elim M N + +lemma empty_eq_empty_right [is_empty n] (M N: matrix m n α) : M = N := subsingleton.elim M N end matrix diff --git a/src/linear_algebra/matrix/nonsingular_inverse.lean b/src/linear_algebra/matrix/nonsingular_inverse.lean index a1f495e7059ce..d0ca561c80cc5 100644 --- a/src/linear_algebra/matrix/nonsingular_inverse.lean +++ b/src/linear_algebra/matrix/nonsingular_inverse.lean @@ -489,6 +489,6 @@ if the determinant is not a unit. A sufficient (but still not necessary) conditi divides `b`. -/ @[simp] lemma mul_vec_cramer (A : matrix n n α) (b : n → α) : A.mul_vec (cramer A b) = A.det • b := -by rw [cramer_eq_adjugate_mul_vec, mul_vec_mul_vec, mul_adjugate, smul_mul_vec_assoc, mul_vec_one] +by rw [cramer_eq_adjugate_mul_vec, mul_vec_mul_vec, mul_adjugate, smul_mul_vec_assoc, one_mul_vec] end matrix From afccd56c2c34fda83f876601d6f55ccaba0b2bc1 Mon Sep 17 00:00:00 2001 From: l534zhan Date: Thu, 15 Jul 2021 09:01:09 +0100 Subject: [PATCH 10/29] change --- src/data/matrix/basic.lean | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index 0a4a77aaba6df..e0399a778dabf 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -397,7 +397,7 @@ instance [has_mul α] [add_comm_monoid α] : has_mul (matrix n n α) := ⟨matri @[simp] theorem mul_eq_mul [has_mul α] [add_comm_monoid α] (M N : matrix n n α) : M * N = M ⬝ N := rfl -theorem mul_apply' [has_mul α] [add_comm_monoid α] {M N : matrix n 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 = dot_product (λ j, M i j) (λ j, N j k) := rfl @[simp] theorem diagonal_neg [decidable_eq n] [add_group α] (d : n → α) : @@ -415,9 +415,15 @@ variables [non_unital_non_assoc_semiring α] @[simp] protected theorem mul_zero (M : matrix m n α) : M ⬝ (0 : matrix n o α) = 0 := by { ext i j, apply dot_product_zero } +@[simp] protected theorem mul_zero' (M : matrix m n α) : M ⬝ (λ i j , 0 : matrix n o α) = 0 := +by { ext i j, apply dot_product_zero } + @[simp] protected theorem zero_mul (M : matrix m n α) : (0 : matrix l m α) ⬝ M = 0 := by { ext i j, apply zero_dot_product } +@[simp] protected theorem zero_mul' (M : matrix m n α) : (λ i j , 0 : matrix l m α) ⬝ M = 0 := +by { ext i j, apply zero_dot_product } + protected theorem mul_add (L : matrix m n α) (M N : matrix n o α) : L ⬝ (M + N) = L ⬝ M + L ⬝ N := by { ext i j, apply dot_product_add } @@ -783,13 +789,13 @@ by { ext, rw [←diagonal_one, vec_mul_diagonal, mul_one] } @[simp] lemma mul_vec_one (A : matrix m n α) : mul_vec A 1 = λ i, ∑ j, A i j := by ext; simp [mul_vec, dot_product] -@[simp] lemma mul_vec_one' (A : matrix m n α) : mul_vec A (λ i, 1) = λ i, ∑ j, A i j := +lemma mul_vec_one' (A : matrix m n α) : mul_vec A (λ i, 1) = λ i, ∑ j, A i j := by ext; simp [mul_vec, dot_product] @[simp] lemma vec_one_mul (A : matrix m n α) : vec_mul 1 A = λ j, ∑ i, A i j := by ext; simp [vec_mul, dot_product] -@[simp] lemma vec_one_mul' (A : matrix m n α) : vec_mul (λ j, 1 : m → α) A = λ j, ∑ i, A i j := +lemma vec_one_mul' (A : matrix m n α) : vec_mul (λ j, 1 : m → α) A = λ j, ∑ i, A i j := by ext; simp [vec_mul, dot_product] end non_assoc_semiring From 1b2ef30e811b4fa6c07a75c06eb10a76ff70ea12 Mon Sep 17 00:00:00 2001 From: l534zhan Date: Tue, 27 Jul 2021 20:14:46 +0100 Subject: [PATCH 11/29] change --- src/data/matrix/basic.lean | 29 ++++------------------------- 1 file changed, 4 insertions(+), 25 deletions(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index 12d1542c97f3a..9e0df9aafadc7 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -31,14 +31,6 @@ variables {m' : o → Type*} [∀ i, fintype (m' i)] variables {n' : o → Type*} [∀ i, fintype (n' i)] variables {R : Type*} {S : Type*} {α : Type v} {β : Type w} -/-- `equiv.perm.to_matrix` converts a permutation `σ : equiv.perm m` to a matrix - containing ones and zeros. This definition is then used to define the Prop `matrix.is_perm`. - `equiv.perm.to_prequiv_to_matrix_eq_to_matrix` proves that - `σ.to_pequiv.to_matrix = σ.to_matrix` in `pequiv.lean`.-/ -def equiv.perm.to_matrix [decidable_eq m] [has_zero α] [has_one α] (σ : equiv.perm m) : -matrix m m α -| i j := if σ i = j then 1 else 0 - namespace matrix instance [inhabited α] : inhabited (matrix m n α) := pi.inhabited _ @@ -137,19 +129,6 @@ protected def is_skewsym [has_neg α] (A : matrix m m α) : Prop := -Aᵀ = A /-- Proposition `matrix.is_Hermitian`. `A.is_Hermitian` means `Aᴴ = A` if `[has_star α]` -/ protected def is_Hermitian [has_star α] (A : matrix m m α) : Prop := Aᴴ = A -/-- Proposition `matrix.is_perm`. - `P.is_perm` means `P` is a permutation matrix. - A new file is probably required for systematically investigating permutation matrices. -/ -protected def is_perm [decidable_eq m] [has_zero α] [has_one α] (P : matrix m m α): Prop := -∃ σ : equiv.perm m, P = equiv.perm.to_matrix σ - -/-- Proposition `matrix.is_perfect_shuffle`. - `P.is_perfect_shuffle` means `P` is a perfect shuffle matrix. - A new file is probably required for systematically investigating perfect shuffle matrices. -/ -protected def is_perfect_shuffle -[decidable_eq m] [has_zero α] [has_one α] (P : matrix m m α) : Prop := -∃ σ : equiv.perm m, (P = equiv.perm.to_matrix σ ∧ ∀ i : m, σ i ≠ i) - -- TODO[gh-6025]: make this an instance once safe to do so lemma subsingleton_of_empty_left [is_empty m] : subsingleton (matrix m n α) := ⟨λ M N, by { ext, exact is_empty_elim i }⟩ @@ -334,16 +313,16 @@ end non_unital_non_assoc_semiring_decidable section non_distrib_ring variables [mul_one_class α] [add_comm_monoid α] -@[simp] lemma dot_product_one (v : n → α) : dot_product v 1 = ∑ i, v i := +lemma dot_product_one (v : n → α) : dot_product v 1 = ∑ i, v i := by simp [dot_product] -@[simp] lemma dot_product_one' (v : n → α) : dot_product v (λ i, 1) = ∑ i, v i := +lemma dot_product_one' (v : n → α) : dot_product v (λ i, 1) = ∑ i, v i := by simp [dot_product] -@[simp] lemma one_dot_product (v : n → α) : dot_product 1 v = ∑ i, v i := +lemma one_dot_product (v : n → α) : dot_product 1 v = ∑ i, v i := by simp [dot_product] -@[simp] lemma one_dot_product' (v : n → α) : dot_product (λ i, 1 : n → α) v = ∑ i, v i := +lemma one_dot_product' (v : n → α) : dot_product (λ i, 1 : n → α) v = ∑ i, v i := by simp [dot_product] @[simp] lemma one_dot_one_eq_card : dot_product (1 : n → α) 1 = fintype.card n := From 7b18a57328df068ed878331e553bedd8d1e50e5f Mon Sep 17 00:00:00 2001 From: l534zhan Date: Tue, 27 Jul 2021 20:16:48 +0100 Subject: [PATCH 12/29] change --- src/data/matrix/pequiv.lean | 7 ------- 1 file changed, 7 deletions(-) diff --git a/src/data/matrix/pequiv.lean b/src/data/matrix/pequiv.lean index 89c404d4b172f..4ff339d17176f 100644 --- a/src/data/matrix/pequiv.lean +++ b/src/data/matrix/pequiv.lean @@ -48,13 +48,6 @@ open_locale matrix def to_matrix [decidable_eq n] [has_zero α] [has_one α] (f : m ≃. n) : matrix m n α | i j := if j ∈ f i then 1 else 0 -/-- `equiv.perm.to_prequiv_to_matrix_eq_to_matrix` proves that - `σ.to_pequiv.to_matrix = σ.to_matrix` for a permutation `σ : equiv.perm m`.-/ -lemma _root_.equiv.perm.to_prequiv_to_matrix_eq_to_matrix -[decidable_eq n] [has_zero α] [has_one α] (σ : equiv.perm n) : -(σ.to_pequiv.to_matrix : matrix n n α)= σ.to_matrix := -by ext i j; simp [pequiv.to_matrix, equiv.perm.to_matrix,equiv.to_pequiv] - 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 From 63623fe4d9d3f9f41ca186060e38d72ab17c7e53 Mon Sep 17 00:00:00 2001 From: l534zhan Date: Fri, 6 Aug 2021 11:19:04 +0100 Subject: [PATCH 13/29] change --- src/data/matrix/basic.lean | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index 9e0df9aafadc7..6c215d9f8bc2e 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -137,13 +137,11 @@ lemma subsingleton_of_empty_left [is_empty m] : subsingleton (matrix m n α) := lemma subsingleton_of_empty_right [is_empty n] : subsingleton (matrix m n α) := ⟨λ M N, by { ext, exact is_empty_elim j }⟩ -local attribute [instance] matrix.subsingleton_of_empty_left matrix.subsingleton_of_empty_right +lemma empty_eq_empty_left [c: is_empty m] (M N: matrix m n α) : M = N := +by {ext, exfalso, apply is_empty_iff.mp c i} -lemma empty_eq_empty_left [is_empty m] (M N: matrix m n α) : M = N := -subsingleton.elim M N - -lemma empty_eq_empty_right [is_empty n] (M N: matrix m n α) : M = N := -subsingleton.elim M N +lemma empty_eq_empty_right [c: is_empty n] (M N: matrix m n α) : M = N := +by {ext, exfalso, apply is_empty_iff.mp c j} end matrix From 8ec73c9a3361de7f3c945bbbd3b067946636623e Mon Sep 17 00:00:00 2001 From: l534zhan Date: Fri, 6 Aug 2021 11:59:23 +0100 Subject: [PATCH 14/29] change --- src/data/matrix/basic.lean | 30 +----------------------------- 1 file changed, 1 insertion(+), 29 deletions(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index 1f63462035230..f38ddda3a47e7 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -39,6 +39,7 @@ instance [has_add α] : has_add (matrix m n α) := pi.has_add instance [add_semigroup α] : add_semigroup (matrix m n α) := pi.add_semigroup instance [add_comm_semigroup α] : add_comm_semigroup (matrix m n α) := pi.add_comm_semigroup instance [has_zero α] : has_zero (matrix m n α) := pi.has_zero +instance [add_zero_class α] : add_zero_class (matrix m n α) := pi.add_zero_class instance [add_monoid α] : add_monoid (matrix m n α) := pi.add_monoid instance [add_comm_monoid α] : add_comm_monoid (matrix m n α) := pi.add_comm_monoid instance [has_neg α] : has_neg (matrix m n α) := pi.has_neg @@ -109,35 +110,6 @@ def col (w : m → α) : matrix m unit α def row (v : n → α) : matrix unit n α | x y := v y -instance [inhabited α] : inhabited (matrix m n α) := pi.inhabited _ -instance [has_add α] : has_add (matrix m n α) := pi.has_add -instance [add_semigroup α] : add_semigroup (matrix m n α) := pi.add_semigroup -instance [add_comm_semigroup α] : add_comm_semigroup (matrix m n α) := pi.add_comm_semigroup -instance [has_zero α] : has_zero (matrix m n α) := pi.has_zero -instance [add_zero_class α] : add_zero_class (matrix m n α) := pi.add_zero_class -instance [add_monoid α] : add_monoid (matrix m n α) := pi.add_monoid -instance [add_comm_monoid α] : add_comm_monoid (matrix m n α) := pi.add_comm_monoid -instance [has_neg α] : has_neg (matrix m n α) := pi.has_neg -instance [has_sub α] : has_sub (matrix m n α) := pi.has_sub -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 -instance [unique α] : unique (matrix m n α) := pi.unique -instance [subsingleton α] : subsingleton (matrix m n α) := pi.subsingleton -instance [nonempty m] [nonempty n] [nontrivial α] : nontrivial (matrix m n α) := -function.nontrivial - -instance [has_scalar R α] : has_scalar R (matrix m n α) := pi.has_scalar -instance [has_scalar R α] [has_scalar S α] [smul_comm_class R S α] : - smul_comm_class R S (matrix m n α) := pi.smul_comm_class -instance [has_scalar R S] [has_scalar R α] [has_scalar S α] [is_scalar_tower R S α] : - is_scalar_tower R S (matrix m n α) := pi.is_scalar_tower -instance [monoid R] [mul_action R α] : - mul_action R (matrix m n α) := pi.mul_action _ -instance [monoid R] [add_monoid α] [distrib_mul_action R α] : - distrib_mul_action R (matrix m n α) := pi.distrib_mul_action _ -instance [semiring R] [add_comm_monoid α] [module R α] : - module R (matrix m n α) := pi.module _ _ _ - @[simp] lemma map_zero [has_zero α] [has_zero β] (f : α → β) (h : f 0 = 0) : (0 : matrix m n α).map f = 0 := by { ext, simp [h], } From 5f6ad37f46ec51a443b00ff8052ff52c9c365298 Mon Sep 17 00:00:00 2001 From: l534zhan Date: Fri, 6 Aug 2021 16:20:34 +0100 Subject: [PATCH 15/29] change --- src/data/matrix/basic.lean | 6 ++++-- src/data/matrix/block.lean | 2 +- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index f38ddda3a47e7..65cd3b10e44f3 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -141,17 +141,19 @@ localized "postfix `ᴴ`:1500 := matrix.conj_transpose" in matrix /-- Proposition `matrix.is_sym`. `A.is_sym` means `Aᵀ = A`. -/ protected def is_sym (A : matrix m m α) : Prop := Aᵀ = A -/-- Proposition `matrix.is_skewsym`. `A.is_skewsym` means `-Aᵀ = A` if `[has_neg α]` -/ +/-- Proposition `matrix.is_skewsym`. `A.is_skewsym` means `-Aᵀ = A` if `[has_neg α]`. -/ protected def is_skewsym [has_neg α] (A : matrix m m α) : Prop := -Aᵀ = A -/-- Proposition `matrix.is_Hermitian`. `A.is_Hermitian` means `Aᴴ = A` if `[has_star α]` -/ +/-- Proposition `matrix.is_Hermitian`. `A.is_Hermitian` means `Aᴴ = A` if `[has_star α]`. -/ protected def is_Hermitian [has_star α] (A : matrix m m α) : Prop := Aᴴ = A -- TODO[gh-6025]: make this an instance once safe to do so +/-- Should be used by adding `local attribute [instance] subsingleton_of_empty_left`. -/ lemma subsingleton_of_empty_left [is_empty m] : subsingleton (matrix m n α) := ⟨λ M N, by { ext, exact is_empty_elim i }⟩ -- TODO[gh-6025]: make this an instance once safe to do so +/-- Should be used by adding `local attribute [instance] subsingleton_of_empty_right`. -/ lemma subsingleton_of_empty_right [is_empty n] : subsingleton (matrix m n α) := ⟨λ M N, by { ext, exact is_empty_elim j }⟩ diff --git a/src/data/matrix/block.lean b/src/data/matrix/block.lean index 497aff6bbd40c..d4ad4a22ddfaf 100644 --- a/src/data/matrix/block.lean +++ b/src/data/matrix/block.lean @@ -32,7 +32,7 @@ open_locale big_operators lemma dot_product_block' [has_mul α] [add_comm_monoid α] (v w : m ⊕ n → α) : dot_product v w = ∑ i, v (sum.inl i) * w (sum.inl i) + ∑ j, v (sum.inr j) * w (sum.inr j) := -by {rw [dot_product, ←fintype.sum_sum_elim], congr, ext (i | j); simp } +by rw [dot_product, fintype.sum_sum_type] lemma dot_product_block [has_mul α] [add_comm_monoid α] (v w : m ⊕ n → α) : dot_product v w = From 20618f9d9133e85175af25d766aa561fa71b67f7 Mon Sep 17 00:00:00 2001 From: l534zhan Date: Fri, 6 Aug 2021 16:21:49 +0100 Subject: [PATCH 16/29] change --- src/data/matrix/basic.lean | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index 65cd3b10e44f3..2a9cc413d1245 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -157,12 +157,6 @@ lemma subsingleton_of_empty_left [is_empty m] : subsingleton (matrix m n α) := lemma subsingleton_of_empty_right [is_empty n] : subsingleton (matrix m n α) := ⟨λ M N, by { ext, exact is_empty_elim j }⟩ -lemma empty_eq_empty_left [c: is_empty m] (M N: matrix m n α) : M = N := -by {ext, exfalso, apply is_empty_iff.mp c i} - -lemma empty_eq_empty_right [c: is_empty n] (M N: matrix m n α) : M = N := -by {ext, exfalso, apply is_empty_iff.mp c j} - end matrix open_locale matrix From 5d8e75369250fd42c2ad8b41836c3624b90c1381 Mon Sep 17 00:00:00 2001 From: l534zhan Date: Fri, 6 Aug 2021 16:24:36 +0100 Subject: [PATCH 17/29] change --- src/data/matrix/basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index 2a9cc413d1245..94d53b5c9f57a 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -1027,13 +1027,13 @@ by { ext, rw [←diagonal_one, mul_vec_diagonal, one_mul] } @[simp] lemma vec_mul_one [decidable_eq m] (v : m → α) : vec_mul v 1 = v := by { ext, rw [←diagonal_one, vec_mul_diagonal, mul_one] } -@[simp] lemma mul_vec_one (A : matrix m n α) : mul_vec A 1 = λ i, ∑ j, A i j := +lemma mul_vec_one (A : matrix m n α) : mul_vec A 1 = λ i, ∑ j, A i j := by ext; simp [mul_vec, dot_product] lemma mul_vec_one' (A : matrix m n α) : mul_vec A (λ i, 1) = λ i, ∑ j, A i j := by ext; simp [mul_vec, dot_product] -@[simp] lemma vec_one_mul (A : matrix m n α) : vec_mul 1 A = λ j, ∑ i, A i j := +lemma vec_one_mul (A : matrix m n α) : vec_mul 1 A = λ j, ∑ i, A i j := by ext; simp [vec_mul, dot_product] lemma vec_one_mul' (A : matrix m n α) : vec_mul (λ j, 1 : m → α) A = λ j, ∑ i, A i j := From 824a8eed9f540bb30056114c498262d5b87b9b55 Mon Sep 17 00:00:00 2001 From: l534zhan Date: Fri, 6 Aug 2021 17:22:52 +0100 Subject: [PATCH 18/29] change --- src/data/matrix/basic.lean | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index 94d53b5c9f57a..0682be81c7545 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -439,15 +439,9 @@ variables [non_unital_non_assoc_semiring α] @[simp] protected theorem mul_zero (M : matrix m n α) : M ⬝ (0 : matrix n o α) = 0 := by { ext i j, apply dot_product_zero } -@[simp] protected theorem mul_zero' (M : matrix m n α) : M ⬝ (λ i j , 0 : matrix n o α) = 0 := -by { ext i j, apply dot_product_zero } - @[simp] protected theorem zero_mul (M : matrix m n α) : (0 : matrix l m α) ⬝ M = 0 := by { ext i j, apply zero_dot_product } -@[simp] protected theorem zero_mul' (M : matrix m n α) : (λ i j , 0 : matrix l m α) ⬝ M = 0 := -by { ext i j, apply zero_dot_product } - protected theorem mul_add (L : matrix m n α) (M N : matrix n o α) : L ⬝ (M + N) = L ⬝ M + L ⬝ N := by { ext i j, apply dot_product_add } From 9bf4a800f53d6bd981005b211a35d5ed791a49ce Mon Sep 17 00:00:00 2001 From: l534zhan <84618936+l534zhan@users.noreply.github.com> Date: Mon, 9 Aug 2021 16:25:22 +0100 Subject: [PATCH 19/29] Update src/data/matrix/basic.lean Co-authored-by: Johan Commelin --- src/data/matrix/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index 0682be81c7545..a7dce784b533e 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -138,7 +138,7 @@ M.transpose.map star localized "postfix `ᴴ`:1500 := matrix.conj_transpose" in matrix -/-- Proposition `matrix.is_sym`. `A.is_sym` means `Aᵀ = A`. -/ +/-- A matrix `A` is *symmetric* if `Aᵀ = A`. -/ protected def is_sym (A : matrix m m α) : Prop := Aᵀ = A /-- Proposition `matrix.is_skewsym`. `A.is_skewsym` means `-Aᵀ = A` if `[has_neg α]`. -/ From 5e32307107b19f5b029dc9003c53b507d14beb1e Mon Sep 17 00:00:00 2001 From: l534zhan <84618936+l534zhan@users.noreply.github.com> Date: Mon, 9 Aug 2021 16:25:33 +0100 Subject: [PATCH 20/29] Update src/data/matrix/block.lean Co-authored-by: Johan Commelin --- src/data/matrix/block.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/data/matrix/block.lean b/src/data/matrix/block.lean index d4ad4a22ddfaf..7698e39d8331b 100644 --- a/src/data/matrix/block.lean +++ b/src/data/matrix/block.lean @@ -35,9 +35,9 @@ dot_product v w = ∑ i, v (sum.inl i) * w (sum.inl i) + ∑ j, v (sum.inr j) * by rw [dot_product, fintype.sum_sum_type] lemma dot_product_block [has_mul α] [add_comm_monoid α] (v w : m ⊕ n → α) : -dot_product v w = -dot_product (λ i, v (sum.inl i)) (λ i, w (sum.inl i)) + -dot_product (λ j, v (sum.inr j)) (λ j, w (sum.inr j)) := + dot_product v w = + dot_product (λ i, v (sum.inl i)) (λ i, w (sum.inl i)) + + dot_product (λ j, v (sum.inr j)) (λ j, w (sum.inr j)) := by simp [dot_product, dot_product_block'] end vector From 33ca4586e45fa9a28bee17813a775b4d339e5bfd Mon Sep 17 00:00:00 2001 From: l534zhan <84618936+l534zhan@users.noreply.github.com> Date: Mon, 9 Aug 2021 16:25:42 +0100 Subject: [PATCH 21/29] Update src/data/matrix/basic.lean Co-authored-by: Johan Commelin --- src/data/matrix/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index a7dce784b533e..5e32879cc0066 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -144,7 +144,7 @@ protected def is_sym (A : matrix m m α) : Prop := Aᵀ = A /-- Proposition `matrix.is_skewsym`. `A.is_skewsym` means `-Aᵀ = A` if `[has_neg α]`. -/ protected def is_skewsym [has_neg α] (A : matrix m m α) : Prop := -Aᵀ = A -/-- Proposition `matrix.is_Hermitian`. `A.is_Hermitian` means `Aᴴ = A` if `[has_star α]`. -/ +/-- A matrix is *Hermitian* if `Aᴴ = A`. -/ protected def is_Hermitian [has_star α] (A : matrix m m α) : Prop := Aᴴ = A -- TODO[gh-6025]: make this an instance once safe to do so From 0b80e3a4e99f974c6a57f0eae7d16b83dc291bef Mon Sep 17 00:00:00 2001 From: l534zhan <84618936+l534zhan@users.noreply.github.com> Date: Mon, 9 Aug 2021 16:25:55 +0100 Subject: [PATCH 22/29] Update src/data/matrix/block.lean Co-authored-by: Johan Commelin --- src/data/matrix/block.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/data/matrix/block.lean b/src/data/matrix/block.lean index 7698e39d8331b..35699e5066446 100644 --- a/src/data/matrix/block.lean +++ b/src/data/matrix/block.lean @@ -31,7 +31,7 @@ section vector open_locale big_operators lemma dot_product_block' [has_mul α] [add_comm_monoid α] (v w : m ⊕ n → α) : -dot_product v w = ∑ i, v (sum.inl i) * w (sum.inl i) + ∑ j, v (sum.inr j) * w (sum.inr j) := + dot_product v w = ∑ i, v (sum.inl i) * w (sum.inl i) + ∑ j, v (sum.inr j) * w (sum.inr j) := by rw [dot_product, fintype.sum_sum_type] lemma dot_product_block [has_mul α] [add_comm_monoid α] (v w : m ⊕ n → α) : From d1a71949622ecd121c007c8fb3c0db10634d66c7 Mon Sep 17 00:00:00 2001 From: l534zhan <84618936+l534zhan@users.noreply.github.com> Date: Mon, 9 Aug 2021 16:26:06 +0100 Subject: [PATCH 23/29] Update src/data/matrix/basic.lean Co-authored-by: Johan Commelin --- src/data/matrix/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index 5e32879cc0066..bca81d9e8a28d 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -141,7 +141,7 @@ localized "postfix `ᴴ`:1500 := matrix.conj_transpose" in matrix /-- A matrix `A` is *symmetric* if `Aᵀ = A`. -/ protected def is_sym (A : matrix m m α) : Prop := Aᵀ = A -/-- Proposition `matrix.is_skewsym`. `A.is_skewsym` means `-Aᵀ = A` if `[has_neg α]`. -/ +/-- A matrix `A` is *skew symmetric* if `-Aᵀ = A`. -/ protected def is_skewsym [has_neg α] (A : matrix m m α) : Prop := -Aᵀ = A /-- A matrix is *Hermitian* if `Aᴴ = A`. -/ From 2ac46f6b8e6ef952238e59230f6ba87e8379dddb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 20 Apr 2023 09:19:49 +0000 Subject: [PATCH 24/29] reduce diff --- src/data/matrix/basic.lean | 39 ++------------------------------------ src/data/matrix/block.lean | 18 ++++-------------- 2 files changed, 6 insertions(+), 51 deletions(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index be31211b6d7b7..fef6d99e2fa56 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -62,43 +62,14 @@ variables {R : Type*} {S : Type*} {α : Type v} {β : Type w} {γ : Type*} namespace matrix -instance [inhabited α] : inhabited (matrix m n α) := pi.inhabited _ -instance [has_add α] : has_add (matrix m n α) := pi.has_add -instance [add_semigroup α] : add_semigroup (matrix m n α) := pi.add_semigroup -instance [add_comm_semigroup α] : add_comm_semigroup (matrix m n α) := pi.add_comm_semigroup -instance [has_zero α] : has_zero (matrix m n α) := pi.has_zero -instance [add_zero_class α] : add_zero_class (matrix m n α) := pi.add_zero_class -instance [add_monoid α] : add_monoid (matrix m n α) := pi.add_monoid -instance [add_comm_monoid α] : add_comm_monoid (matrix m n α) := pi.add_comm_monoid -instance [has_neg α] : has_neg (matrix m n α) := pi.has_neg -instance [has_sub α] : has_sub (matrix m n α) := pi.has_sub -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 -instance [unique α] : unique (matrix m n α) := pi.unique -instance [subsingleton α] : subsingleton (matrix m n α) := pi.subsingleton -instance [nonempty m] [nonempty n] [nontrivial α] : nontrivial (matrix m n α) := -function.nontrivial - -instance [has_scalar R α] : has_scalar R (matrix m n α) := pi.has_scalar -instance [has_scalar R α] [has_scalar S α] [smul_comm_class R S α] : - smul_comm_class R S (matrix m n α) := pi.smul_comm_class -instance [has_scalar R S] [has_scalar R α] [has_scalar S α] [is_scalar_tower R S α] : - is_scalar_tower R S (matrix m n α) := pi.is_scalar_tower -instance [monoid R] [mul_action R α] : - mul_action R (matrix m n α) := pi.mul_action _ -instance [monoid R] [add_monoid α] [distrib_mul_action R α] : - distrib_mul_action R (matrix m n α) := pi.distrib_mul_action _ -instance [semiring R] [add_comm_monoid α] [module R α] : - module R (matrix m n α) := pi.module _ _ _ - section ext - variables {M N : matrix m n α} theorem ext_iff : (∀ i j, M i j = N i j) ↔ M = N := ⟨λ h, funext $ λ i, funext $ h i, λ h, by simp [h]⟩ -@[ext] theorem ext : (∀ i j, M i j = N i j) → M = N := ext_iff.mp +@[ext] theorem ext : (∀ i j, M i j = N i j) → M = N := +ext_iff.mp end ext @@ -1356,15 +1327,9 @@ by { ext, rw [←diagonal_one, vec_mul_diagonal, mul_one] } lemma mul_vec_one (A : matrix m n α) : mul_vec A 1 = λ i, ∑ j, A i j := by ext; simp [mul_vec, dot_product] -lemma mul_vec_one' (A : matrix m n α) : mul_vec A (λ i, 1) = λ i, ∑ j, A i j := -by ext; simp [mul_vec, dot_product] - lemma vec_one_mul (A : matrix m n α) : vec_mul 1 A = λ j, ∑ i, A i j := by ext; simp [vec_mul, dot_product] -lemma vec_one_mul' (A : matrix m n α) : vec_mul (λ j, 1 : m → α) A = λ j, ∑ i, A i j := -by ext; simp [vec_mul, dot_product] - end non_assoc_semiring section non_unital_non_assoc_ring diff --git a/src/data/matrix/block.lean b/src/data/matrix/block.lean index 2976d9f30f8b7..6d40f968863d1 100644 --- a/src/data/matrix/block.lean +++ b/src/data/matrix/block.lean @@ -27,25 +27,15 @@ import data.matrix.basic 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 -section vector - -open_locale big_operators - -lemma dot_product_block' [has_mul α] [add_comm_monoid α] (v w : m ⊕ n → α) : - dot_product v w = ∑ i, v (sum.inl i) * w (sum.inl i) + ∑ j, v (sum.inr j) * w (sum.inr j) := -by rw [dot_product, fintype.sum_sum_type] - lemma dot_product_block [has_mul α] [add_comm_monoid α] (v w : m ⊕ n → α) : dot_product v w = - dot_product (λ i, v (sum.inl i)) (λ i, w (sum.inl i)) + - dot_product (λ j, v (sum.inr j)) (λ j, w (sum.inr j)) := -by simp [dot_product, dot_product_block'] - -end vector + dot_product (λ i, v (sum.inl i)) (λ i, w (sum.inl i)) + + dot_product (λ j, v (sum.inr j)) (λ j, w (sum.inr j)) := +fintype.sum_sum_type _ section block_matrices From 01f8479a78405be5c9d04c04134516bccc84e39c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 20 Apr 2023 10:39:45 +0000 Subject: [PATCH 25/29] fix one_dot_product_one --- src/data/matrix/basic.lean | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index fef6d99e2fa56..3d566a05d7b8c 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -478,9 +478,6 @@ variables [mul_one_class α] [add_comm_monoid α] lemma dot_product_one (v : n → α) : dot_product v 1 = ∑ i, v i := by simp [dot_product] lemma one_dot_product (v : n → α) : dot_product 1 v = ∑ i, v i := by simp [dot_product] -@[simp] lemma one_dot_one : dot_product (1 : n → α) 1 = fintype.card n := -by simp [dot_product, fintype.card] - end mul_one_class section non_unital_non_assoc_semiring @@ -544,6 +541,14 @@ by convert finset.sum_eq_single i (λ j _, this j) _ using 1; simp end non_unital_non_assoc_semiring_decidable +section non_assoc_semiring +variables [non_assoc_semiring α] + +@[simp] lemma one_dot_product_one : dot_product (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 → α) From a5a1888b3d56b0c7cf35153bbc4e28cb635a32d1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 20 Apr 2023 10:40:25 +0000 Subject: [PATCH 26/29] fix mul_vec_one --- src/data/matrix/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index 3d566a05d7b8c..0505d66557783 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -1321,7 +1321,7 @@ by { rw matrix.mul_assoc, simpa only [mul_apply, dot_product, mul_vec] } end non_unital_semiring section non_assoc_semiring -variables [fintype m] [decidable_eq m] [non_assoc_semiring α] +variables [fintype m] [fintype n] [decidable_eq m] [non_assoc_semiring α] @[simp] lemma one_mul_vec (v : m → α) : mul_vec 1 v = v := by { ext, rw [←diagonal_one, mul_vec_diagonal, one_mul] } From 758e25e565498c862017c922b33a1ea5cc964e91 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 20 Apr 2023 15:15:28 +0000 Subject: [PATCH 27/29] fix data.matrix.block --- src/data/matrix/block.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/data/matrix/block.lean b/src/data/matrix/block.lean index 6d40f968863d1..77e3529dd9e38 100644 --- a/src/data/matrix/block.lean +++ b/src/data/matrix/block.lean @@ -31,7 +31,7 @@ open_locale big_operators matrix namespace matrix -lemma dot_product_block [has_mul α] [add_comm_monoid α] (v w : m ⊕ n → α) : +lemma dot_product_block [fintype m] [fintype n] [has_mul α] [add_comm_monoid α] (v w : m ⊕ n → α) : dot_product v w = dot_product (λ i, v (sum.inl i)) (λ i, w (sum.inl i)) + dot_product (λ j, v (sum.inr j)) (λ j, w (sum.inr j)) := From 239f5ab0c0ebe53535feb6dcd76986c6bad1d59f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 20 Apr 2023 17:14:31 +0000 Subject: [PATCH 28/29] =?UTF-8?q?use=20`=E2=AC=9D=E1=B5=A5`=20notation?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/data/matrix/basic.lean | 6 +++--- src/data/matrix/block.lean | 4 +--- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index 0505d66557783..d500a70b4dcfa 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -475,8 +475,8 @@ by simp [dot_product] section mul_one_class variables [mul_one_class α] [add_comm_monoid α] -lemma dot_product_one (v : n → α) : dot_product v 1 = ∑ i, v i := by simp [dot_product] -lemma one_dot_product (v : n → α) : dot_product 1 v = ∑ i, v i := by simp [dot_product] +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 @@ -544,7 +544,7 @@ end non_unital_non_assoc_semiring_decidable section non_assoc_semiring variables [non_assoc_semiring α] -@[simp] lemma one_dot_product_one : dot_product (1 : n → α) 1 = fintype.card n := +@[simp] lemma one_dot_product_one : (1 : n → α) ⬝ᵥ 1 = fintype.card n := by simp [dot_product, fintype.card] end non_assoc_semiring diff --git a/src/data/matrix/block.lean b/src/data/matrix/block.lean index 77e3529dd9e38..bc311dd65413f 100644 --- a/src/data/matrix/block.lean +++ b/src/data/matrix/block.lean @@ -32,9 +32,7 @@ open_locale big_operators matrix namespace matrix lemma dot_product_block [fintype m] [fintype n] [has_mul α] [add_comm_monoid α] (v w : m ⊕ n → α) : - dot_product v w = - dot_product (λ i, v (sum.inl i)) (λ i, w (sum.inl i)) + - dot_product (λ j, v (sum.inr j)) (λ j, w (sum.inr j)) := + v ⬝ᵥ w = v ∘ sum.inl ⬝ᵥ w ∘ sum.inl + v ∘ sum.inr ⬝ᵥ w ∘ sum.inr := fintype.sum_sum_type _ section block_matrices From ef549bdd6c4f3374881c6b03399e61cc21635769 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Fri, 21 Apr 2023 10:27:13 +0000 Subject: [PATCH 29/29] fix lint --- src/data/matrix/basic.lean | 22 +++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index d500a70b4dcfa..d681d732fc588 100644 --- a/src/data/matrix/basic.lean +++ b/src/data/matrix/basic.lean @@ -1321,7 +1321,15 @@ by { rw matrix.mul_assoc, simpa only [mul_apply, dot_product, mul_vec] } end non_unital_semiring section non_assoc_semiring -variables [fintype m] [fintype n] [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] } @@ -1329,12 +1337,6 @@ by { ext, rw [←diagonal_one, mul_vec_diagonal, one_mul] } @[simp] lemma vec_mul_one (v : m → α) : vec_mul v 1 = v := by { ext, rw [←diagonal_one, vec_mul_diagonal, mul_one] } -lemma mul_vec_one (A : matrix m n α) : mul_vec A 1 = λ i, ∑ j, A i j := -by ext; simp [mul_vec, dot_product] - -lemma vec_one_mul (A : matrix m n α) : vec_mul 1 A = λ j, ∑ i, A i j := -by ext; simp [vec_mul, dot_product] - end non_assoc_semiring section non_unital_non_assoc_ring @@ -1838,10 +1840,11 @@ lemma submatrix_vec_mul_equiv [fintype l] [fintype m] [non_unital_non_assoc_semi 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, @@ -1851,10 +1854,11 @@ begin 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,