Commit 2023-04-28 06:56 3f22ac3c

View on Github →

chore: forward-port leanprover-community/mathlib#18842 (#3675)

Estimated changes

Modified Mathlib/Data/Matrix/Block.lean

added theorem Matrix.blockDiagonal'_inj

added theorem Matrix.blockDiagonal'_injective

added theorem Matrix.blockDiagonal_inj

added theorem Matrix.blockDiagonal_injective

added theorem Matrix.ext_iff_blocks

added theorem Matrix.fromBlocks_inj