Block

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

Statistics

Metric	Count
Definitions `BlockTriangular`, `invertibleToBlock`	2
Theorems `add`, `add_iff_left`, `add_iff_right`, `comp`, `det`, `det_fintype`, `inv_toBlock`, `map`, `mul`, `neg`, `sub`, `sub_iff_left`, `sub_iff_right`, `submatrix`, `toBlock_inverse_mul_toBlock_eq_one`, `transpose`, `blockTriangular_blockDiagonal`, `blockTriangular_blockDiagonal'`, `blockTriangular_diagonal`, `blockTriangular_inv_of_blockTriangular`, `blockTriangular_one`, `blockTriangular_reindex_iff`, `blockTriangular_single`, `blockTriangular_single'`, `blockTriangular_transpose_iff`, `blockTriangular_transvection`, `blockTriangular_transvection'`, `blockTriangular_zero`, `det_matrixOfPolynomials`, `det_of_lowerTriangular`, `det_of_upperTriangular`, `det_toBlock`, `det_toSquareBlock_id`, `equiv_block_det`, `matrixOfPolynomials_blockTriangular`, `toBlock_inverse_eq_zero`, `twoBlockTriangular_det`, `twoBlockTriangular_det'`, `upper_two_blockTriangular`	39
Total	41

Matrix

Definitions

Name	Category	Theorems
`BlockTriangular` 📖	MathDef	17 math math: `blockTriangular_blockDiagonal`, `blockTriangular_diagonal`, `blockTriangular_transvection'`, `upper_two_blockTriangular`, `charmatrix_blockTriangular_iff`, `blockTriangular_zero`, `blockTriangular_single`, `InnerProductSpace.gramSchmidtOrthonormalBasis_inv_blockTriangular`, `blockTriangular_transpose_iff`, `Algebra.Norm.Transitivity.mul_auxMat_blockTriangular`, `matrixOfPolynomials_blockTriangular`, `blockTriangular_transvection`, `blockTriangular_blockDiagonal'`, `Algebra.Norm.Transitivity.auxMat_blockTriangular`, `blockTriangular_single'`, `blockTriangular_one`, `blockTriangular_reindex_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`blockTriangular_blockDiagonal` 📖	mathematical	—	`BlockTriangular` `Preorder.toLT` `blockDiagonal`	—	`blockDiagonal'_eq_blockDiagonal` `blockTriangular_blockDiagonal'`
`blockTriangular_blockDiagonal'` 📖	mathematical	—	`BlockTriangular` `Preorder.toLT` `blockDiagonal'`	—	`blockDiagonal'_apply_ne` `ne_of_lt`
`blockTriangular_diagonal` 📖	mathematical	—	`BlockTriangular` `Preorder.toLT` `diagonal`	—	`diagonal_apply_ne'` `ne_of_lt`
`blockTriangular_inv_of_blockTriangular` 📖	mathematical	`BlockTriangular` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`Matrix` `inv`	—	`Finset.Nonempty.image` `Finset.univ_nonempty` `Finset.mem_image_of_mem` `Finset.mem_univ` `LE.le.eq_or_lt` `Finset.le_max'` `Eq.ge` `toBlock_inverse_eq_zero` `BlockTriangular.submatrix` `image_subtype_univ_ssubset_image_univ` `Finset.max'_mem` `lt_irrefl` `LT.lt.trans` `BlockTriangular.inv_toBlock`
`blockTriangular_one` 📖	mathematical	—	`BlockTriangular` `Preorder.toLT` `Matrix` `one`	—	`blockTriangular_diagonal`
`blockTriangular_reindex_iff` 📖	mathematical	—	`BlockTriangular` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `reindex`	—	`submatrix_submatrix` `Equiv.symm_comp_self` `submatrix_id_id` `BlockTriangular.submatrix` `Equiv.self_comp_symm`
`blockTriangular_single` 📖	mathematical	`Preorder.toLE`	`BlockTriangular` `Preorder.toLT` `single`	—	`single_apply_of_ne` `LT.lt.false` `LE.le.trans_lt`
`blockTriangular_single'` 📖	mathematical	`Preorder.toLE`	`BlockTriangular` `OrderDual` `OrderDual.instLT` `Preorder.toLT` `single` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	`blockTriangular_single` `OrderDual.toDual_le_toDual`
`blockTriangular_transpose_iff` 📖	mathematical	—	`BlockTriangular` `OrderDual` `OrderDual.instLT` `transpose` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	`forall_swap`
`blockTriangular_transvection` 📖	mathematical	`Preorder.toLE`	`BlockTriangular` `Preorder.toLT` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `transvection`	—	`BlockTriangular.add` `blockTriangular_one` `blockTriangular_single`
`blockTriangular_transvection'` 📖	mathematical	`Preorder.toLE`	`BlockTriangular` `OrderDual` `OrderDual.instLT` `Preorder.toLT` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `transvection` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	`BlockTriangular.add` `blockTriangular_one` `blockTriangular_single'`
`blockTriangular_zero` 📖	mathematical	—	`BlockTriangular` `Matrix` `zero`	—	—
`det_matrixOfPolynomials` 📖	mathematical	`Polynomial.natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.Monic`	`det` `Fin.fintype` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `Polynomial.coeff` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`det_of_upperTriangular` `matrixOfPolynomials_blockTriangular` `Finset.prod_congr` `of_apply` `Polynomial.coeff_natDegree` `Polynomial.Monic.leadingCoeff` `Finset.prod_const_one`
`det_of_lowerTriangular` 📖	mathematical	`BlockTriangular` `OrderDual` `OrderDual.instLT` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	`det` `Finset.prod` `CommRing.toCommMonoid` `Finset.univ`	—	`det_transpose` `det_of_upperTriangular` `BlockTriangular.transpose`
`det_of_upperTriangular` 📖	mathematical	`BlockTriangular` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`det` `Finset.prod` `CommRing.toCommMonoid` `Finset.univ`	—	`BlockTriangular.det` `Finset.prod_congr` `Finset.image_id` `det_toSquareBlock_id`
`det_toBlock` 📖	mathematical	—	`det` `instFintypeSum` `Subtype.fintype` `fromBlocks` `toBlock`	—	`det_reindex_self` `det_apply'`
`det_toSquareBlock_id` 📖	mathematical	—	`det` `Subtype.fintype` `toSquareBlock`	—	`det_unique`
`equiv_block_det` 📖	mathematical	—	`det` `Subtype.fintype` `toSquareBlockProp`	—	`det_reindex_self`
`matrixOfPolynomials_blockTriangular` 📖	mathematical	`Polynomial.natDegree`	`BlockTriangular` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `Polynomial.coeff`	—	`Polynomial.coeff_eq_zero_of_natDegree_lt`
`toBlock_inverse_eq_zero` 📖	mathematical	`BlockTriangular` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`toBlock` `Matrix` `inv` `Preorder.toLE` `zero`	—	`toBlock_mul_eq_add` `inv_mul_of_invertible` `toBlock_one_disjoint` `disjoint_iff_inf_le` `ext` `lt_of_lt_of_le` `le_of_not_gt` `mul_zero` `add_zero` `not_lt` `zero_mul` `mul_inv_cancel_right_of_invertible`
`twoBlockTriangular_det` 📖	mathematical	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`det` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Subtype.fintype` `toSquareBlockProp`	—	`det_toBlock` `ext` `det_fromBlocks_zero₂₁`
`twoBlockTriangular_det'` 📖	mathematical	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`det` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Subtype.fintype` `toSquareBlockProp`	—	`twoBlockTriangular_det` `mul_comm` `equiv_block_det`
`upper_two_blockTriangular` 📖	mathematical	`Preorder.toLT`	`BlockTriangular` `fromBlocks` `Matrix` `zero`	—	`LT.lt.not_gt`

Matrix.BlockTriangular

Definitions

Name	Category	Theorems
`invertibleToBlock` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`Matrix.BlockTriangular` `AddZero.toZero` `AddZeroClass.toAddZero`	`Matrix` `Matrix.add` `AddZero.toAdd`	—	`zero_add`
`add_iff_left` 📖	mathematical	`Matrix.BlockTriangular` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`Matrix` `Matrix.add` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`add_sub_cancel_right` `sub` `add`
`add_iff_right` 📖	mathematical	`Matrix.BlockTriangular` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`Matrix` `Matrix.add` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`neg_add_cancel_left` `add` `neg`
`comp` 📖	mathematical	`Matrix.BlockTriangular` `Matrix` `Matrix.zero`	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Matrix.comp`	—	—
`det` 📖	mathematical	`Matrix.BlockTriangular` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`Matrix.det` `Finset.prod` `CommRing.toCommMonoid` `Finset.image` `Finset.univ` `Subtype.fintype` `Matrix.toSquareBlock`	—	`Finset.eraseInduction` `isEmpty_or_nonempty` `Matrix.coe_det_isEmpty` `Finset.prod_congr` `Finset.univ_eq_empty` `instIsEmptySubtype` `Finset.prod_const_one` `Finset.Nonempty.image` `Finset.univ_nonempty` `Matrix.twoBlockTriangular_det'` `lt_of_le_of_ne` `Finset.le_max'` `Finset.mem_image_of_mem` `Finset.mem_univ` `Finset.insert_erase` `Finset.max'_mem` `Finset.prod_insert` `Finset.notMem_erase` `submatrix` `image_subtype_ne_univ_eq_image_erase` `ne_of_eq_of_ne` `Finset.ne_of_mem_erase` `Matrix.det_reindex_self`
`det_fintype` 📖	mathematical	`Matrix.BlockTriangular` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`Matrix.det` `Finset.prod` `CommRing.toCommMonoid` `Finset.univ` `Subtype.fintype` `Matrix.toSquareBlock`	—	`det` `Finset.prod_subset` `Finset.subset_univ` `Finset.mem_image` `Finset.mem_univ` `Matrix.det_isEmpty`
`inv_toBlock` 📖	mathematical	`Matrix.BlockTriangular` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`Matrix` `Matrix.inv` `Subtype.fintype` `LinearOrder.toDecidableLT` `Matrix.toBlock`	—	`Matrix.inv_eq_left_inv` `toBlock_inverse_mul_toBlock_eq_one`
`map` 📖	mathematical	`Matrix.BlockTriangular`	`Matrix.map` `DFunLike.coe`	—	`map_zero`
`mul` 📖	mathematical	`Matrix.BlockTriangular` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	`Finset.sum_eq_zero` `MulZeroClass.zero_mul` `lt_of_lt_of_le` `MulZeroClass.mul_zero`
`neg` 📖	mathematical	`Matrix.BlockTriangular` `NegZeroClass.toZero`	`Matrix` `Matrix.neg` `NegZeroClass.toNeg`	—	`Matrix.neg_apply` `neg_zero`
`sub` 📖	mathematical	`Matrix.BlockTriangular` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass`	`Matrix` `Matrix.sub` `SubNegMonoid.toSub` `SubNegZeroMonoid.toSubNegMonoid`	—	`sub_zero`
`sub_iff_left` 📖	mathematical	`Matrix.BlockTriangular` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`Matrix` `Matrix.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`sub_add_cancel` `add` `sub`
`sub_iff_right` 📖	mathematical	`Matrix.BlockTriangular` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`Matrix` `Matrix.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`neg_sub` `sub_add_cancel` `add` `neg` `sub`
`submatrix` 📖	mathematical	`Matrix.BlockTriangular`	`Matrix.submatrix`	—	—
`toBlock_inverse_mul_toBlock_eq_one` 📖	mathematical	`Matrix.BlockTriangular` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Subtype.fintype` `LinearOrder.toDecidableLT` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.toBlock` `Matrix.inv` `Matrix.one` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	`Matrix.toBlock_mul_eq_add` `Matrix.inv_mul_of_invertible` `Matrix.toBlock_one_self` `Matrix.ext` `lt_of_lt_of_le` `le_of_not_gt` `Matrix.mul_zero` `add_zero`
`transpose` 📖	mathematical	`Matrix.BlockTriangular`	`OrderDual` `OrderDual.instLT` `Matrix.transpose` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	—

---

← Back to Index