Commit 2023-04-03 13:22 ab2cc874

View on Github →

feat: port Data.Matrix.Block (#3232)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Matrix/Block.lean

added def Matrix.IsTwoBlockDiagonal

added def Matrix.blockDiag'

added def Matrix.blockDiag'AddMonoidHom

added theorem Matrix.blockDiag'_add

added theorem Matrix.blockDiag'_apply

added theorem Matrix.blockDiag'_blockDiagonal'

added theorem Matrix.blockDiag'_conjTranspose

added theorem Matrix.blockDiag'_diagonal

added theorem Matrix.blockDiag'_map

added theorem Matrix.blockDiag'_neg

added theorem Matrix.blockDiag'_one

added theorem Matrix.blockDiag'_smul

added theorem Matrix.blockDiag'_sub

added theorem Matrix.blockDiag'_transpose

added theorem Matrix.blockDiag'_zero

added def Matrix.blockDiag

added def Matrix.blockDiagAddMonoidHom

added theorem Matrix.blockDiag_add

added theorem Matrix.blockDiag_apply

added theorem Matrix.blockDiag_blockDiagonal

added theorem Matrix.blockDiag_conjTranspose

added theorem Matrix.blockDiag_diagonal

added theorem Matrix.blockDiag_map

added theorem Matrix.blockDiag_neg

added theorem Matrix.blockDiag_one

added theorem Matrix.blockDiag_smul

added theorem Matrix.blockDiag_sub

added theorem Matrix.blockDiag_transpose

added theorem Matrix.blockDiag_zero

added def Matrix.blockDiagonal'

added def Matrix.blockDiagonal'AddMonoidHom

added def Matrix.blockDiagonal'RingHom

added theorem Matrix.blockDiagonal'_add

added theorem Matrix.blockDiagonal'_apply'

added theorem Matrix.blockDiagonal'_apply

added theorem Matrix.blockDiagonal'_apply_eq

added theorem Matrix.blockDiagonal'_apply_ne

added theorem Matrix.blockDiagonal'_conjTranspose

added theorem Matrix.blockDiagonal'_diagonal

added theorem Matrix.blockDiagonal'_eq_blockDiagonal

added theorem Matrix.blockDiagonal'_map

added theorem Matrix.blockDiagonal'_mul

added theorem Matrix.blockDiagonal'_neg

added theorem Matrix.blockDiagonal'_one

added theorem Matrix.blockDiagonal'_pow

added theorem Matrix.blockDiagonal'_smul

added theorem Matrix.blockDiagonal'_sub

added theorem Matrix.blockDiagonal'_submatrix_eq_blockDiagonal

added theorem Matrix.blockDiagonal'_transpose

added theorem Matrix.blockDiagonal'_zero

added def Matrix.blockDiagonal

added def Matrix.blockDiagonalAddMonoidHom

added def Matrix.blockDiagonalRingHom

added theorem Matrix.blockDiagonal_add

added theorem Matrix.blockDiagonal_apply'

added theorem Matrix.blockDiagonal_apply

added theorem Matrix.blockDiagonal_apply_eq

added theorem Matrix.blockDiagonal_apply_ne

added theorem Matrix.blockDiagonal_conjTranspose

added theorem Matrix.blockDiagonal_diagonal

added theorem Matrix.blockDiagonal_map

added theorem Matrix.blockDiagonal_mul

added theorem Matrix.blockDiagonal_neg

added theorem Matrix.blockDiagonal_one

added theorem Matrix.blockDiagonal_pow

added theorem Matrix.blockDiagonal_smul

added theorem Matrix.blockDiagonal_sub

added theorem Matrix.blockDiagonal_transpose

added theorem Matrix.blockDiagonal_zero

added def Matrix.fromBlocks

added theorem Matrix.fromBlocks_add

added theorem Matrix.fromBlocks_apply₁₁

added theorem Matrix.fromBlocks_apply₁₂

added theorem Matrix.fromBlocks_apply₂₁

added theorem Matrix.fromBlocks_apply₂₂

added theorem Matrix.fromBlocks_conjTranspose

added theorem Matrix.fromBlocks_diagonal

added theorem Matrix.fromBlocks_map

added theorem Matrix.fromBlocks_mulVec

added theorem Matrix.fromBlocks_multiply

added theorem Matrix.fromBlocks_neg

added theorem Matrix.fromBlocks_one

added theorem Matrix.fromBlocks_smul

added theorem Matrix.fromBlocks_submatrix_sum_swap_left

added theorem Matrix.fromBlocks_submatrix_sum_swap_right

added theorem Matrix.fromBlocks_submatrix_sum_swap_sum_swap

added theorem Matrix.fromBlocks_to_blocks

added theorem Matrix.fromBlocks_transpose

added def Matrix.toBlock

added theorem Matrix.toBlock_apply

added theorem Matrix.toBlock_diagonal_disjoint

added theorem Matrix.toBlock_diagonal_self

added theorem Matrix.toBlock_mul_eq_add

added theorem Matrix.toBlock_mul_eq_mul

added theorem Matrix.toBlock_one_disjoint

added theorem Matrix.toBlock_one_self

added def Matrix.toBlocks₁₁

added def Matrix.toBlocks₁₂

added def Matrix.toBlocks₂₁

added def Matrix.toBlocks₂₂

added def Matrix.toSquareBlock

added def Matrix.toSquareBlockProp

added theorem Matrix.toSquareBlockProp_def

added theorem Matrix.toSquareBlock_def

added theorem Matrix.to_blocks_from_blocks₁₁

added theorem Matrix.to_blocks_from_blocks₁₂

added theorem Matrix.to_blocks_from_blocks₂₁

added theorem Matrix.to_blocks_from_blocks₂₂

added theorem Matrix.vecMul_fromBlocks

Modified Mathlib/Order/PropInstances.lean