From e46fa5133b7f5cca1c1bc3f91a55d25ea46d9360 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 4 May 2023 11:23:09 +0000 Subject: [PATCH] chore: forward-port leanprover-community/mathlib#18879 (#3741) --- Mathlib/Data/Matrix/Block.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Mathlib/Data/Matrix/Block.lean b/Mathlib/Data/Matrix/Block.lean index f9d5a92873b37..7b959e00fc21f 100644 --- a/Mathlib/Data/Matrix/Block.lean +++ b/Mathlib/Data/Matrix/Block.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ellen Arlt, Blair Shi, Sean Leather, Mario Carneiro, Johan Commelin ! This file was ported from Lean 3 source module data.matrix.block -! leanprover-community/mathlib commit b5665fd3fb2a80ee05ff42b6031ef2055b8f9d85 +! leanprover-community/mathlib commit c060baa79af5ca092c54b8bf04f0f10592f59489 ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ @@ -234,6 +234,12 @@ theorem fromBlocks_neg [Neg R] (A : Matrix n l R) (B : Matrix n m R) (C : Matrix cases i <;> cases j <;> simp [fromBlocks] #align matrix.from_blocks_neg Matrix.fromBlocks_neg +@[simp] +theorem fromBlocks_zero [Zero α] : fromBlocks (0 : Matrix n l α) 0 0 (0 : Matrix o m α) = 0 := by + ext (i j) + rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> rfl +#align matrix.from_blocks_zero Matrix.fromBlocks_zero + theorem fromBlocks_add [Add α] (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (A' : Matrix n l α) (B' : Matrix n m α) (C' : Matrix o l α) (D' : Matrix o m α) :