Block

📁 Source: Mathlib/Data/Matrix/Block.lean

Statistics

Metric	Count
Definitions `IsTwoBlockDiagonal`, `blockDiag`, `blockDiag'`, `blockDiag'AddMonoidHom`, `blockDiagAddMonoidHom`, `blockDiagonal`, `blockDiagonal'`, `blockDiagonal'AddMonoidHom`, `blockDiagonal'RingHom`, `blockDiagonalAddMonoidHom`, `blockDiagonalRingHom`, `fromBlocks`, `toBlock`, `toBlocks₁₁`, `toBlocks₁₂`, `toBlocks₂₁`, `toBlocks₂₂`, `toSquareBlock`, `toSquareBlockProp`	19
Theorems `blockDiag'AddMonoidHom_apply`, `blockDiag'_add`, `blockDiag'_apply`, `blockDiag'_blockDiagonal'`, `blockDiag'_conjTranspose`, `blockDiag'_diagonal`, `blockDiag'_map`, `blockDiag'_neg`, `blockDiag'_one`, `blockDiag'_smul`, `blockDiag'_sub`, `blockDiag'_transpose`, `blockDiag'_zero`, `blockDiagAddMonoidHom_apply`, `blockDiag_add`, `blockDiag_apply`, `blockDiag_blockDiagonal`, `blockDiag_conjTranspose`, `blockDiag_diagonal`, `blockDiag_map`, `blockDiag_neg`, `blockDiag_one`, `blockDiag_smul`, `blockDiag_sub`, `blockDiag_transpose`, `blockDiag_zero`, `blockDiagonal'AddMonoidHom_apply`, `blockDiagonal'RingHom_apply`, `blockDiagonal'_add`, `blockDiagonal'_apply`, `blockDiagonal'_apply'`, `blockDiagonal'_apply_eq`, `blockDiagonal'_apply_ne`, `blockDiagonal'_conjTranspose`, `blockDiagonal'_diagonal`, `blockDiagonal'_eq_blockDiagonal`, `blockDiagonal'_inj`, `blockDiagonal'_injective`, `blockDiagonal'_map`, `blockDiagonal'_mul`, `blockDiagonal'_neg`, `blockDiagonal'_one`, `blockDiagonal'_pow`, `blockDiagonal'_smul`, `blockDiagonal'_sub`, `blockDiagonal'_submatrix_eq_blockDiagonal`, `blockDiagonal'_transpose`, `blockDiagonal'_zero`, `blockDiagonalAddMonoidHom_apply`, `blockDiagonalRingHom_apply`, `blockDiagonal_add`, `blockDiagonal_apply`, `blockDiagonal_apply'`, `blockDiagonal_apply_eq`, `blockDiagonal_apply_ne`, `blockDiagonal_conjTranspose`, `blockDiagonal_diagonal`, `blockDiagonal_inj`, `blockDiagonal_injective`, `blockDiagonal_map`, `blockDiagonal_mul`, `blockDiagonal_neg`, `blockDiagonal_one`, `blockDiagonal_pow`, `blockDiagonal_smul`, `blockDiagonal_sub`, `blockDiagonal_transpose`, `blockDiagonal_zero`, `comp_diagonal`, `comp_toSquareBlock`, `dotProduct_block`, `ext_iff_blocks`, `fromBlocks_add`, `fromBlocks_apply₁₁`, `fromBlocks_apply₁₂`, `fromBlocks_apply₂₁`, `fromBlocks_apply₂₂`, `fromBlocks_conjTranspose`, `fromBlocks_diagonal`, `fromBlocks_diagonal_pow`, `fromBlocks_inj`, `fromBlocks_map`, `fromBlocks_mulVec`, `fromBlocks_multiply`, `fromBlocks_neg`, `fromBlocks_one`, `fromBlocks_smul`, `fromBlocks_submatrix_sum_swap_left`, `fromBlocks_submatrix_sum_swap_right`, `fromBlocks_submatrix_sum_swap_sum_swap`, `fromBlocks_toBlocks`, `fromBlocks_transpose`, `fromBlocks_zero`, `map_toSquareBlock`, `toBlock_apply`, `toBlock_diagonal_disjoint`, `toBlock_diagonal_self`, `toBlock_mul_eq_add`, `toBlock_mul_eq_mul`, `toBlock_one_disjoint`, `toBlock_one_self`, `toBlocks_fromBlocks₁₁`, `toBlocks_fromBlocks₁₂`, `toBlocks_fromBlocks₂₁`, `toBlocks_fromBlocks₂₂`, `toBlocks₁₁_diagonal`, `toBlocks₁₂_diagonal`, `toBlocks₂₁_diagonal`, `toBlocks₂₂_diagonal`, `toSquareBlockProp_def`, `toSquareBlock_def`, `vecMul_fromBlocks`	112
Total	131

Matrix

Definitions

Name	Category	Theorems
`IsTwoBlockDiagonal` 📖	MathDef	3 math math: `Pivot.exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec`, `Pivot.isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow`, `Pivot.exists_isTwoBlockDiagonal_of_ne_zero`
`blockDiag` 📖	CompOp	16 math math: `Continuous.matrix_blockDiag`, `blockDiag_one`, `Summable.matrix_blockDiag`, `blockDiag_add`, `blockDiag_transpose`, `blockDiag_zero`, `blockDiag_blockDiagonal`, `blockDiag_map`, `blockDiag_diagonal`, `HasSum.matrix_blockDiag`, `blockDiag_apply`, `blockDiag_sub`, `blockDiagAddMonoidHom_apply`, `blockDiag_smul`, `blockDiag_neg`, `blockDiag_conjTranspose`
`blockDiag'` 📖	CompOp	16 math math: `blockDiag'_diagonal`, `HasSum.matrix_blockDiag'`, `blockDiag'_zero`, `blockDiag'_one`, `Summable.matrix_blockDiag'`, `blockDiag'_neg`, `blockDiag'_add`, `blockDiag'_smul`, `blockDiag'_blockDiagonal'`, `blockDiag'AddMonoidHom_apply`, `Continuous.matrix_blockDiag'`, `blockDiag'_conjTranspose`, `blockDiag'_apply`, `blockDiag'_map`, `blockDiag'_sub`, `blockDiag'_transpose`
`blockDiag'AddMonoidHom` 📖	CompOp	1 math math: `blockDiag'AddMonoidHom_apply`
`blockDiagAddMonoidHom` 📖	CompOp	1 math math: `blockDiagAddMonoidHom_apply`
`blockDiagonal` 📖	CompOp	46 math math: `natCast_kronecker`, `blockDiagonal_apply_ne`, `kronecker_natCast`, `blockTriangular_blockDiagonal`, `one_kronecker`, `blockDiagonal_transpose`, `blockDiagonal_tsum`, `Summable.matrix_blockDiagonal`, `blockDiagonal_injective`, `blockDiagonal_inj`, `blockDiagonal_neg`, `kroneckerMap_diagonal_right`, `blockDiagonal_map`, `blockDiag_blockDiagonal`, `blockDiagonal_conjTranspose`, `diagonal_kroneckerTMul`, `Continuous.matrix_blockDiagonal`, `blockDiagonal'_submatrix_eq_blockDiagonal`, `blockDiagonal_smul`, `blockDiagonal_mul`, `kronecker_one`, `blockDiagonal_sub`, `kronecker_ofNat`, `blockDiagonal_zero`, `blockDiagonal_add`, `exp_blockDiagonal`, `det_blockDiagonal`, `blockDiagonal_apply_eq`, `diagonal_kronecker`, `Algebra.smulTower_leftMulMatrix_algebraMap`, `blockDiagonal_diagonal`, `blockDiagonal_apply'`, `blockDiagonal_pow`, `kroneckerTMul_diagonal`, `ofNat_kronecker`, `trace_blockDiagonal`, `comp_diagonal`, `blockDiagonalRingHom_apply`, `HasSum.matrix_blockDiagonal`, `blockDiagonalAddMonoidHom_apply`, `blockDiagonal'_eq_blockDiagonal`, `blockDiagonal_apply`, `kronecker_diagonal`, `kroneckerMap_diagonal_left`, `summable_matrix_blockDiagonal`, `blockDiagonal_one`
`blockDiagonal'` 📖	CompOp	32 math math: `trace_blockDiagonal'`, `blockDiagonal'RingHom_apply`, `blockDiagonal'_map`, `blockDiagonal'_apply`, `blockDiagonal'_one`, `HasSum.matrix_blockDiagonal'`, `blockDiagonal'_apply_ne`, `blockDiagonal'_neg`, `blockDiagonal'_diagonal`, `Summable.matrix_blockDiagonal'`, `blockDiagonal'_injective`, `summable_matrix_blockDiagonal'`, `blockDiagonal'_inj`, `blockDiagonal'_mul`, `blockDiagonal'_apply_eq`, `blockDiagonal'_submatrix_eq_blockDiagonal`, `blockDiagonal'AddMonoidHom_apply`, `blockDiagonal'_zero`, `blockDiag'_blockDiagonal'`, `blockDiagonal'_add`, `blockDiagonal'_transpose`, `LinearMap.toMatrix_directSum_collectedBasis_eq_blockDiagonal'`, `blockDiagonal'_apply'`, `blockDiagonal'_sub`, `exp_blockDiagonal'`, `blockTriangular_blockDiagonal'`, `Continuous.matrix_blockDiagonal'`, `blockDiagonal'_eq_blockDiagonal`, `blockDiagonal'_tsum`, `blockDiagonal'_smul`, `blockDiagonal'_conjTranspose`, `blockDiagonal'_pow`
`blockDiagonal'AddMonoidHom` 📖	CompOp	1 math math: `blockDiagonal'AddMonoidHom_apply`
`blockDiagonal'RingHom` 📖	CompOp	1 math math: `blockDiagonal'RingHom_apply`
`blockDiagonalAddMonoidHom` 📖	CompOp	1 math math: `blockDiagonalAddMonoidHom_apply`
`blockDiagonalRingHom` 📖	CompOp	1 math math: `blockDiagonalRingHom_apply`
`fromBlocks` 📖	CompOp	76 math math: `RootPairing.GeckConstruction.h_def`, `fromBlocks_apply₁₁`, `invOf_fromBlocks₂₂_eq`, `IsHermitian.fromBlocks₂₂`, `fromBlocks_apply₁₂`, `fromBlocks_apply₂₂`, `toBlocks_fromBlocks₂₁`, `IsDiag.fromBlocks`, `inv_fromBlocks_zero₁₂_of_isUnit_iff`, `fromBlocks_eq_of_invertible₁₁`, `fromBlocks_toBlocks`, `PosDef.fromBlocks₁₁`, `fromBlocks_submatrix_sum_swap_left`, `LieAlgebra.Orthogonal.jb_transform`, `upper_two_blockTriangular`, `LieAlgebra.Orthogonal.indefiniteDiagonal_assoc`, `fromRows_fromCols_eq_fromBlocks`, `fromBlocks_conjTranspose`, `fromBlocks_submatrix_sum_swap_sum_swap`, `isUnit_fromBlocks_zero₂₁`, `fromBlocks_mul_fromRows`, `toBlocks_fromBlocks₁₂`, `charpoly_fromBlocks_zero₂₁`, `fromBlocks_add`, `charmatrix_fromBlocks`, `fromBlocks_neg`, `vecMul_fromBlocks`, `fromBlocks_submatrix_sum_swap_right`, `fromBlocks_inj`, `schur_complement_eq₂₂`, `fromBlocks_mulVec`, `TransvectionStruct.mul_sumInl_toMatrix_prod`, `fromBlocks_apply₂₁`, `fromRows_mul_fromCols`, `det_fromBlocks₁₁`, `det_fromBlocks_one₁₁`, `fromBlocks_transpose`, `invOf_fromBlocks_zero₁₂_eq`, `LieAlgebra.Orthogonal.s_as_blocks`, `isUnit_fromBlocks_iff_of_invertible₂₂`, `fromBlocks_diagonal`, `fromBlocks_map`, `det_toBlock`, `fromBlocks_eq_of_invertible₂₂`, `schur_complement_eq₁₁`, `toBlocks_fromBlocks₁₁`, `det_fromBlocks_one₂₂`, `isUnit_fromBlocks_zero₁₂`, `isUnit_fromBlocks_iff_of_invertible₁₁`, `LinearMap.toMatrix_prodMap`, `fromBlocks_one`, `PosDef.fromBlocks₂₂`, `isHermitian_fromBlocks_iff`, `charpoly_fromBlocks_zero₁₂`, `det_fromBlocks₂₂`, `det_fromBlocks_zero₁₂`, `inv_fromBlocks_zero₂₁_of_isUnit_iff`, `IsHermitian.fromBlocks₁₁`, `isSymm_fromBlocks_iff`, `det_fromBlocks_zero₂₁`, `Continuous.matrix_fromBlocks`, `invOf_fromBlocks_zero₂₁_eq`, `IsSymm.fromBlocks`, `TransvectionStruct.sumInl_toMatrix_prod_mul`, `fromBlocks_smul`, `isDiag_fromBlocks_iff`, `fromBlocks_multiply`, `fromBlocks_zero`, `LieAlgebra.Orthogonal.pb_inv`, `TransvectionStruct.toMatrix_sumInl`, `IsHermitian.fromBlocks`, `fromCols_mul_fromBlocks`, `invOf_fromBlocks₁₁_eq`, `toBlocks_fromBlocks₂₂`, `fromBlocks_diagonal_pow`, `fromCols_fromRows_eq_fromBlocks`
`toBlock` 📖	CompOp	11 math math: `toBlock_one_disjoint`, `toBlock_diagonal_disjoint`, `toBlock_mul_eq_add`, `toBlock_mul_eq_mul`, `BlockTriangular.toBlock_inverse_mul_toBlock_eq_one`, `det_toBlock`, `toBlock_diagonal_self`, `toBlock_inverse_eq_zero`, `toBlock_one_self`, `BlockTriangular.inv_toBlock`, `toBlock_apply`
`toBlocks₁₁` 📖	CompOp	4 math math: `fromBlocks_toBlocks`, `ext_iff_blocks`, `toBlocks₁₁_diagonal`, `toBlocks_fromBlocks₁₁`
`toBlocks₁₂` 📖	CompOp	4 math math: `fromBlocks_toBlocks`, `ext_iff_blocks`, `toBlocks_fromBlocks₁₂`, `toBlocks₁₂_diagonal`
`toBlocks₂₁` 📖	CompOp	4 math math: `toBlocks_fromBlocks₂₁`, `fromBlocks_toBlocks`, `ext_iff_blocks`, `toBlocks₂₁_diagonal`
`toBlocks₂₂` 📖	CompOp	4 math math: `fromBlocks_toBlocks`, `ext_iff_blocks`, `toBlocks₂₂_diagonal`, `toBlocks_fromBlocks₂₂`
`toSquareBlock` 📖	CompOp	13 math math: `toSquareBlock_def`, `charmatrix_toSquareBlock`, `Algebra.Norm.Transitivity.comp_det_mul_pow`, `map_toSquareBlock`, `comp_toSquareBlock`, `BlockTriangular.det`, `Algebra.Norm.Transitivity.mul_auxMat_toSquareBlock_eq`, `det_toSquareBlock_id`, `Algebra.Norm.Transitivity.auxMat_toSquareBlock_ne`, `BlockTriangular.det_fintype`, `Algebra.Norm.Transitivity.auxMat_toSquareBlock_eq`, `BlockTriangular.charpoly`, `Algebra.Norm.Transitivity.det_mul_corner_pow`
`toSquareBlockProp` 📖	CompOp	4 math math: `twoBlockTriangular_det`, `twoBlockTriangular_det'`, `toSquareBlockProp_def`, `equiv_block_det`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`blockDiag'AddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Matrix` `AddZeroClass.toAddZero` `addZeroClass` `Pi.addZeroClass` `AddMonoidHom.instFunLike` `blockDiag'AddMonoidHom` `blockDiag'`	—	—
`blockDiag'_add` 📖	mathematical	—	`blockDiag'` `Matrix` `add` `Pi.instAdd`	—	—
`blockDiag'_apply` 📖	mathematical	—	`blockDiag'`	—	—
`blockDiag'_blockDiagonal'` 📖	mathematical	—	`blockDiag'` `blockDiagonal'`	—	`ext` `blockDiagonal'_apply_eq`
`blockDiag'_conjTranspose` 📖	mathematical	—	`blockDiag'` `conjTranspose`	—	`ext`
`blockDiag'_diagonal` 📖	mathematical	—	`blockDiag'` `diagonal` `Sigma.instDecidableEqSigma`	—	`ext` `Decidable.eq_or_ne` `blockDiag'_apply` `diagonal_apply_eq` `diagonal_apply_ne`
`blockDiag'_map` 📖	mathematical	—	`blockDiag'` `map`	—	—
`blockDiag'_neg` 📖	mathematical	—	`blockDiag'` `Matrix` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Pi.instNeg`	—	`map_neg` `AddMonoidHom.instAddMonoidHomClass`
`blockDiag'_one` 📖	mathematical	—	`blockDiag'` `Matrix` `one` `Sigma.instDecidableEqSigma` `Pi.instOne`	—	`blockDiag'_diagonal`
`blockDiag'_smul` 📖	mathematical	—	`blockDiag'` `Matrix` `smul` `Pi.instSMul`	—	—
`blockDiag'_sub` 📖	mathematical	—	`blockDiag'` `Matrix` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `Pi.instSub`	—	`map_sub` `AddMonoidHom.instAddMonoidHomClass`
`blockDiag'_transpose` 📖	mathematical	—	`blockDiag'` `transpose`	—	`ext`
`blockDiag'_zero` 📖	mathematical	—	`blockDiag'` `Matrix` `zero` `Pi.instZero`	—	—
`blockDiagAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Matrix` `AddZeroClass.toAddZero` `addZeroClass` `Pi.addZeroClass` `AddMonoidHom.instFunLike` `blockDiagAddMonoidHom` `blockDiag`	—	—
`blockDiag_add` 📖	mathematical	—	`blockDiag` `Matrix` `add` `Pi.instAdd`	—	—
`blockDiag_apply` 📖	mathematical	—	`blockDiag`	—	—
`blockDiag_blockDiagonal` 📖	mathematical	—	`blockDiag` `blockDiagonal`	—	`ext` `blockDiagonal_apply_eq`
`blockDiag_conjTranspose` 📖	mathematical	—	`blockDiag` `conjTranspose`	—	`ext`
`blockDiag_diagonal` 📖	mathematical	—	`blockDiag` `diagonal`	—	`ext` `Decidable.eq_or_ne` `blockDiag_apply` `diagonal_apply_eq` `diagonal_apply_ne` `Prod.fst_eq_iff`
`blockDiag_map` 📖	mathematical	—	`blockDiag` `map`	—	—
`blockDiag_neg` 📖	mathematical	—	`blockDiag` `Matrix` `neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Pi.instNeg`	—	`map_neg` `AddMonoidHom.instAddMonoidHomClass`
`blockDiag_one` 📖	mathematical	—	`blockDiag` `Matrix` `one` `Pi.instOne`	—	`blockDiag_diagonal`
`blockDiag_smul` 📖	mathematical	—	`blockDiag` `Matrix` `smul` `Function.hasSMul`	—	—
`blockDiag_sub` 📖	mathematical	—	`blockDiag` `Matrix` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `Pi.instSub`	—	`map_sub` `AddMonoidHom.instAddMonoidHomClass`
`blockDiag_transpose` 📖	mathematical	—	`blockDiag` `transpose`	—	`ext`
`blockDiag_zero` 📖	mathematical	—	`blockDiag` `Matrix` `zero` `Pi.instZero`	—	—
`blockDiagonal'AddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Matrix` `AddZeroClass.toAddZero` `Pi.addZeroClass` `addZeroClass` `AddMonoidHom.instFunLike` `blockDiagonal'AddMonoidHom` `blockDiagonal'` `AddZero.toZero`	—	—
`blockDiagonal'RingHom_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Matrix` `Pi.nonAssocSemiring` `nonAssocSemiring` `Sigma.instFintype` `Sigma.instDecidableEqSigma` `RingHom.instFunLike` `blockDiagonal'RingHom` `blockDiagonal'` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	—
`blockDiagonal'_add` 📖	mathematical	—	`blockDiagonal'` `AddZero.toZero` `AddZeroClass.toAddZero` `Pi.instAdd` `Matrix` `add` `AddZero.toAdd`	—	`ext` `add_zero`
`blockDiagonal'_apply` 📖	mathematical	—	`blockDiagonal'`	—	—
`blockDiagonal'_apply'` 📖	mathematical	—	`blockDiagonal'`	—	—
`blockDiagonal'_apply_eq` 📖	mathematical	—	`blockDiagonal'`	—	—
`blockDiagonal'_apply_ne` 📖	mathematical	—	`blockDiagonal'`	—	—
`blockDiagonal'_conjTranspose` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `blockDiagonal'` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`blockDiagonal'_transpose` `blockDiagonal'_map` `star_zero`
`blockDiagonal'_diagonal` 📖	mathematical	—	`blockDiagonal'` `diagonal` `Sigma.instDecidableEqSigma`	—	`ext` `Decidable.eq_or_ne`
`blockDiagonal'_eq_blockDiagonal` 📖	mathematical	—	`blockDiagonal` `blockDiagonal'`	—	—
`blockDiagonal'_inj` 📖	mathematical	—	`blockDiagonal'`	—	`blockDiagonal'_injective`
`blockDiagonal'_injective` 📖	mathematical	—	`Matrix` `blockDiagonal'`	—	`blockDiag'_blockDiagonal'`
`blockDiagonal'_map` 📖	mathematical	—	`map` `blockDiagonal'`	—	`ext`
`blockDiagonal'_mul` 📖	mathematical	—	`blockDiagonal'` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Sigma.instFintype`	—	`ext` `Finset.sum_congr` `Finset.sum_sigma` `Fintype.sum_eq_single` `Finset.sum_eq_zero` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `Finset.sum_const_zero`
`blockDiagonal'_neg` 📖	mathematical	—	`blockDiagonal'` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Pi.instNeg` `Matrix` `neg` `NegZeroClass.toNeg`	—	`map_neg` `AddMonoidHom.instAddMonoidHomClass`
`blockDiagonal'_one` 📖	mathematical	—	`blockDiagonal'` `Pi.instOne` `Matrix` `one` `Sigma.instDecidableEqSigma`	—	`blockDiagonal'_diagonal`
`blockDiagonal'_pow` 📖	mathematical	—	`blockDiagonal'` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Pi.instPow` `Matrix` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `Sigma.instFintype` `Sigma.instDecidableEqSigma`	—	`map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`blockDiagonal'_smul` 📖	mathematical	—	`blockDiagonal'` `Pi.instSMul` `Matrix` `smul` `SMulZeroClass.toSMul`	—	`ext` `smul_zero`
`blockDiagonal'_sub` 📖	mathematical	—	`blockDiagonal'` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Pi.instSub` `Matrix` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`map_sub` `AddMonoidHom.instAddMonoidHomClass`
`blockDiagonal'_submatrix_eq_blockDiagonal` 📖	mathematical	—	`submatrix` `blockDiagonal'` `Prod.toSigma` `blockDiagonal`	—	`ext`
`blockDiagonal'_transpose` 📖	mathematical	—	`transpose` `blockDiagonal'`	—	`ext`
`blockDiagonal'_zero` 📖	mathematical	—	`blockDiagonal'` `Pi.instZero` `Matrix` `zero`	—	`ext`
`blockDiagonalAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Matrix` `AddZeroClass.toAddZero` `Pi.addZeroClass` `addZeroClass` `AddMonoidHom.instFunLike` `blockDiagonalAddMonoidHom` `blockDiagonal` `AddZero.toZero`	—	—
`blockDiagonalRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Matrix` `Pi.nonAssocSemiring` `nonAssocSemiring` `instFintypeProd` `RingHom.instFunLike` `blockDiagonalRingHom` `blockDiagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	—
`blockDiagonal_add` 📖	mathematical	—	`blockDiagonal` `AddZero.toZero` `AddZeroClass.toAddZero` `Pi.instAdd` `Matrix` `add` `AddZero.toAdd`	—	`ext` `add_zero`
`blockDiagonal_apply` 📖	mathematical	—	`blockDiagonal`	—	—
`blockDiagonal_apply'` 📖	mathematical	—	`blockDiagonal`	—	—
`blockDiagonal_apply_eq` 📖	mathematical	—	`blockDiagonal`	—	—
`blockDiagonal_apply_ne` 📖	mathematical	—	`blockDiagonal`	—	—
`blockDiagonal_conjTranspose` 📖	mathematical	—	`conjTranspose` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `blockDiagonal` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`blockDiagonal_transpose` `blockDiagonal_map` `star_zero`
`blockDiagonal_diagonal` 📖	mathematical	—	`blockDiagonal` `diagonal`	—	`ext`
`blockDiagonal_inj` 📖	mathematical	—	`blockDiagonal`	—	`blockDiagonal_injective`
`blockDiagonal_injective` 📖	mathematical	—	`Matrix` `blockDiagonal`	—	`blockDiag_blockDiagonal`
`blockDiagonal_map` 📖	mathematical	—	`map` `blockDiagonal`	—	`ext`
`blockDiagonal_mul` 📖	mathematical	—	`blockDiagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instFintypeProd`	—	`ext` `Finset.sum_congr` `Finset.sum_product` `mul_ite` `ite_mul` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero` `Finset.sum_ite_eq'` `Finset.sum_const_zero`
`blockDiagonal_neg` 📖	mathematical	—	`blockDiagonal` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Pi.instNeg` `Matrix` `neg` `NegZeroClass.toNeg`	—	`map_neg` `AddMonoidHom.instAddMonoidHomClass`
`blockDiagonal_one` 📖	mathematical	—	`blockDiagonal` `Pi.instOne` `Matrix` `one`	—	`blockDiagonal_diagonal`
`blockDiagonal_pow` 📖	mathematical	—	`blockDiagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Pi.instPow` `Matrix` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `instFintypeProd`	—	`map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`blockDiagonal_smul` 📖	mathematical	—	`blockDiagonal` `Function.hasSMul` `Matrix` `smul` `SMulZeroClass.toSMul`	—	`ext` `smul_zero`
`blockDiagonal_sub` 📖	mathematical	—	`blockDiagonal` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Pi.instSub` `Matrix` `sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`map_sub` `AddMonoidHom.instAddMonoidHomClass`
`blockDiagonal_transpose` 📖	mathematical	—	`transpose` `blockDiagonal`	—	`ext`
`blockDiagonal_zero` 📖	mathematical	—	`blockDiagonal` `Pi.instZero` `Matrix` `zero`	—	`ext`
`comp_diagonal` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `comp` `diagonal` `zero` `reindex` `Equiv.prodComm` `blockDiagonal`	—	`ext` `ite_apply`
`comp_toSquareBlock` 📖	mathematical	—	`toSquareBlock` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `comp` `reindex` `Equiv.symm` `Equiv.prodSubtypeFstEquivSubtypeProd`	—	—
`dotProduct_block` 📖	mathematical	—	`dotProduct` `instFintypeSum` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`Fintype.sum_sum_type`
`ext_iff_blocks` 📖	mathematical	—	`toBlocks₁₁` `toBlocks₁₂` `toBlocks₂₁` `toBlocks₂₂`	—	`fromBlocks_toBlocks`
`fromBlocks_add` 📖	mathematical	—	`Matrix` `add` `fromBlocks`	—	`ext`
`fromBlocks_apply₁₁` 📖	mathematical	—	`fromBlocks`	—	—
`fromBlocks_apply₁₂` 📖	mathematical	—	`fromBlocks`	—	—
`fromBlocks_apply₂₁` 📖	mathematical	—	`fromBlocks`	—	—
`fromBlocks_apply₂₂` 📖	mathematical	—	`fromBlocks`	—	—
`fromBlocks_conjTranspose` 📖	mathematical	—	`conjTranspose` `fromBlocks`	—	`fromBlocks_transpose` `fromBlocks_map`
`fromBlocks_diagonal` 📖	mathematical	—	`fromBlocks` `diagonal` `Matrix` `zero`	—	`ext`
`fromBlocks_diagonal_pow` 📖	mathematical	—	`Matrix` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `instFintypeSum` `fromBlocks` `zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`ext` `pow_zero` `one_apply_ne` `pow_succ` `fromBlocks_multiply` `mul_zero` `add_zero` `zero_mul` `zero_add`
`fromBlocks_inj` 📖	mathematical	—	`fromBlocks`	—	`ext_iff_blocks`
`fromBlocks_map` 📖	mathematical	—	`map` `fromBlocks`	—	`ext`
`fromBlocks_mulVec` 📖	mathematical	—	`mulVec` `instFintypeSum` `fromBlocks` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	`Finset.sum_congr` `Fintype.sum_sum_type`
`fromBlocks_multiply` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `instFintypeSum` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `fromBlocks` `add` `Distrib.toAdd`	—	`ext` `Finset.sum_congr` `Fintype.sum_sum_type`
`fromBlocks_neg` 📖	mathematical	—	`Matrix` `neg` `fromBlocks`	—	`ext`
`fromBlocks_one` 📖	mathematical	—	`fromBlocks` `Matrix` `one` `zero`	—	`ext` `one_apply_ne`
`fromBlocks_smul` 📖	mathematical	—	`Matrix` `smul` `fromBlocks`	—	`ext`
`fromBlocks_submatrix_sum_swap_left` 📖	mathematical	—	`submatrix` `fromBlocks`	—	`ext`
`fromBlocks_submatrix_sum_swap_right` 📖	mathematical	—	`submatrix` `fromBlocks`	—	`ext`
`fromBlocks_submatrix_sum_swap_sum_swap` 📖	mathematical	—	`submatrix` `fromBlocks`	—	`fromBlocks_submatrix_sum_swap_right` `fromBlocks_submatrix_sum_swap_left` `submatrix_id_id`
`fromBlocks_toBlocks` 📖	mathematical	—	`fromBlocks` `toBlocks₁₁` `toBlocks₁₂` `toBlocks₂₁` `toBlocks₂₂`	—	`ext`
`fromBlocks_transpose` 📖	mathematical	—	`transpose` `fromBlocks`	—	`ext`
`fromBlocks_zero` 📖	mathematical	—	`fromBlocks` `Matrix` `zero`	—	`ext`
`map_toSquareBlock` 📖	mathematical	—	`toSquareBlock` `map`	—	`submatrix_map`
`toBlock_apply` 📖	mathematical	—	`toBlock`	—	—
`toBlock_diagonal_disjoint` 📖	mathematical	`Disjoint` `Pi.partialOrder` `Prop.partialOrder` `Pi.instOrderBot` `Prop.le` `HeytingAlgebra.toOrderBot` `Prop.instHeytingAlgebra`	`toBlock` `diagonal` `Matrix` `zero`	—	`ext` `Disjoint.le_bot` `diagonal_apply_ne`
`toBlock_diagonal_self` 📖	mathematical	—	`toBlock` `diagonal`	—	`ext` `diagonal_apply_eq` `diagonal.congr_simp` `diagonal_apply_ne` `Subtype.val_injective`
`toBlock_mul_eq_add` 📖	mathematical	—	`toBlock` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `add` `Distrib.toAdd` `Subtype.fintype`	—	`ext` `Fintype.sum_subtype_add_sum_subtype`
`toBlock_mul_eq_mul` 📖	mathematical	—	`toBlock` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Top.top` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra` `Subtype.fintype` `Prop.decidablePredTop`	—	`ext` `Finset.sum_congr` `Finset.sum_subtype`
`toBlock_one_disjoint` 📖	mathematical	`Disjoint` `Pi.partialOrder` `Prop.partialOrder` `Pi.instOrderBot` `Prop.le` `HeytingAlgebra.toOrderBot` `Prop.instHeytingAlgebra`	`toBlock` `Matrix` `one` `zero`	—	`toBlock_diagonal_disjoint`
`toBlock_one_self` 📖	mathematical	—	`toBlock` `Matrix` `one`	—	`toBlock_diagonal_self`
`toBlocks_fromBlocks₁₁` 📖	mathematical	—	`toBlocks₁₁` `fromBlocks`	—	—
`toBlocks_fromBlocks₁₂` 📖	mathematical	—	`toBlocks₁₂` `fromBlocks`	—	—
`toBlocks_fromBlocks₂₁` 📖	mathematical	—	`toBlocks₂₁` `fromBlocks`	—	—
`toBlocks_fromBlocks₂₂` 📖	mathematical	—	`toBlocks₂₂` `fromBlocks`	—	—
`toBlocks₁₁_diagonal` 📖	mathematical	—	`toBlocks₁₁` `diagonal`	—	—
`toBlocks₁₂_diagonal` 📖	mathematical	—	`toBlocks₁₂` `diagonal` `Matrix` `zero`	—	—
`toBlocks₂₁_diagonal` 📖	mathematical	—	`toBlocks₂₁` `diagonal` `Matrix` `zero`	—	—
`toBlocks₂₂_diagonal` 📖	mathematical	—	`toBlocks₂₂` `diagonal`	—	—
`toSquareBlockProp_def` 📖	mathematical	—	`toSquareBlockProp` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of`	—	—
`toSquareBlock_def` 📖	mathematical	—	`toSquareBlock` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of`	—	—
`vecMul_fromBlocks` 📖	mathematical	—	`vecMul` `instFintypeSum` `fromBlocks` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	`Finset.sum_congr` `Fintype.sum_sum_type`

---

← Back to Index