Matrix

📁 Source: Mathlib/Topology/Instances/Matrix.lean

Statistics

Metric	Count
Definitions instTopologicalSpaceMatrix	1
Theorems dotProduct, matrix_adjugate, matrix_blockDiag, matrix_blockDiag', matrix_blockDiagonal, matrix_blockDiagonal', matrix_conjTranspose, matrix_cramer, matrix_det, matrix_diag, matrix_diagonal, matrix_elem, matrix_fromBlocks, matrix_map, matrix_mul, matrix_mulVec, matrix_reindex, matrix_replicateCol, matrix_replicateRow, matrix_submatrix, matrix_trace, matrix_transpose, matrix_updateCol, matrix_updateRow, matrix_vecMul, matrix_vecMulVec, matrix_blockDiag, matrix_blockDiag', matrix_blockDiagonal, matrix_blockDiagonal', matrix_conjTranspose, matrix_diag, matrix_diagonal, matrix_transpose, blockDiagonal'_tsum, blockDiagonal_tsum, conjTranspose_tsum, diagonal_tsum, topologicalRing, transpose_tsum, matrix_blockDiag, matrix_blockDiag', matrix_blockDiagonal, matrix_blockDiagonal', matrix_conjTranspose, matrix_diag, matrix_diagonal, matrix_transpose, matrix_map, matrix_map, matrix_map, matrix_map, continuousAt_matrix_inv, continuous_matrix, continuous_matrix_diag, instContinuousAddMatrix, instContinuousConstSMulMatrix, instContinuousMulMatrixOfContinuousAdd, instContinuousNegMatrix, instContinuousSMulMatrix, instContinuousStarMatrix, instDiscreteTopologyMatrixOfFinite, instIsTopologicalAddGroupMatrix, instIsTopologicalSemiringMatrix, instT2SpaceMatrix, summable_matrix_blockDiagonal, summable_matrix_blockDiagonal', summable_matrix_conjTranspose, summable_matrix_diagonal, summable_matrix_transpose	70
Total	71

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dotProduct 📖	mathematical	Continuous Pi.topologicalSpace	Continuous dotProduct	—	continuous_finset_sum comp' continuous_mul prodMk continuous_apply
matrix_adjugate 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Continuous Matrix instTopologicalSpaceMatrix Matrix.adjugate	—	continuous_matrix matrix_det matrix_updateCol matrix_transpose continuous_const
matrix_blockDiag 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Continuous Pi.topologicalSpace Matrix instTopologicalSpaceMatrix Matrix.blockDiag	—	continuous_pi continuous_matrix matrix_elem
matrix_blockDiag' 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Continuous Pi.topologicalSpace Matrix instTopologicalSpaceMatrix Matrix.blockDiag'	—	continuous_pi continuous_matrix matrix_elem
matrix_blockDiagonal 📖	mathematical	Continuous Pi.topologicalSpace Matrix instTopologicalSpaceMatrix	Continuous Matrix instTopologicalSpaceMatrix Matrix.blockDiagonal	—	continuous_matrix if_const matrix_elem comp continuous_apply continuous_zero
matrix_blockDiagonal' 📖	mathematical	Continuous Pi.topologicalSpace Matrix instTopologicalSpaceMatrix	Continuous Matrix instTopologicalSpaceMatrix Matrix.blockDiagonal'	—	continuous_matrix matrix_elem comp continuous_apply continuous_const
matrix_conjTranspose 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Continuous Matrix instTopologicalSpaceMatrix Matrix.conjTranspose	—	matrix_map matrix_transpose ContinuousStar.continuous_star
matrix_cramer 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix Pi.topologicalSpace	Continuous Pi.topologicalSpace DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.Function.module Semiring.toModule LinearMap.instFunLike Matrix.cramer	—	continuous_pi matrix_det matrix_updateCol
matrix_det 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Continuous Matrix.det	—	Matrix.det_apply continuous_finset_sum IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing const_smul Units.continuousConstSMul AddGroup.continuousConstSMul_int IsSemitopologicalRing.toIsTopologicalAddGroup continuous_finset_prod IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring matrix_elem
matrix_diag 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Continuous Pi.topologicalSpace Matrix.diag	—	continuous_pi matrix_elem
matrix_diagonal 📖	mathematical	Continuous Pi.topologicalSpace	Continuous Matrix instTopologicalSpaceMatrix Matrix.diagonal	—	continuous_matrix if_const comp continuous_apply continuous_zero
matrix_elem 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Continuous	—	comp continuous_apply_apply
matrix_fromBlocks 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Continuous Matrix instTopologicalSpaceMatrix Matrix.fromBlocks	—	continuous_matrix matrix_elem
matrix_map 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Continuous Matrix instTopologicalSpaceMatrix Matrix.map	—	continuous_matrix comp matrix_elem
matrix_mul 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Continuous Matrix instTopologicalSpaceMatrix Matrix.instHMulOfFintypeOfMulOfAddCommMonoid	—	continuous_matrix continuous_finset_sum mul matrix_elem
matrix_mulVec 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix Pi.topologicalSpace	Continuous Pi.topologicalSpace Matrix.mulVec	—	continuous_pi dotProduct comp continuous_apply
matrix_reindex 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Continuous Matrix instTopologicalSpaceMatrix DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Matrix.reindex	—	matrix_submatrix
matrix_replicateCol 📖	mathematical	Continuous Pi.topologicalSpace	Continuous Matrix instTopologicalSpaceMatrix Matrix.replicateCol	—	continuous_matrix comp continuous_apply
matrix_replicateRow 📖	mathematical	Continuous Pi.topologicalSpace	Continuous Matrix instTopologicalSpaceMatrix Matrix.replicateRow	—	continuous_matrix comp continuous_apply
matrix_submatrix 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Continuous Matrix instTopologicalSpaceMatrix Matrix.submatrix	—	continuous_matrix matrix_elem
matrix_trace 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Continuous Matrix.trace	—	continuous_finset_sum matrix_elem
matrix_transpose 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Continuous Matrix instTopologicalSpaceMatrix Matrix.transpose	—	continuous_matrix matrix_elem
matrix_updateCol 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix Pi.topologicalSpace	Continuous Matrix instTopologicalSpaceMatrix Matrix.updateCol	—	continuous_matrix comp continuous_apply update
matrix_updateRow 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix Pi.topologicalSpace	Continuous Matrix instTopologicalSpaceMatrix Matrix.updateRow	—	update
matrix_vecMul 📖	mathematical	Continuous Pi.topologicalSpace Matrix instTopologicalSpaceMatrix	Continuous Pi.topologicalSpace Matrix.vecMul	—	continuous_pi dotProduct matrix_elem
matrix_vecMulVec 📖	mathematical	Continuous Pi.topologicalSpace	Continuous Matrix instTopologicalSpaceMatrix Matrix.vecMulVec	—	continuous_matrix mul comp continuous_apply

HasSum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
matrix_blockDiag 📖	mathematical	HasSum Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix	HasSum Pi.addCommMonoid Matrix Matrix.addCommMonoid Pi.topologicalSpace instTopologicalSpaceMatrix Matrix.blockDiag	—	map AddMonoidHom.instAddMonoidHomClass Continuous.matrix_blockDiag continuous_id
matrix_blockDiag' 📖	mathematical	HasSum Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix	HasSum Pi.addCommMonoid Matrix Matrix.addCommMonoid Pi.topologicalSpace instTopologicalSpaceMatrix Matrix.blockDiag'	—	map AddMonoidHom.instAddMonoidHomClass Continuous.matrix_blockDiag' continuous_id
matrix_blockDiagonal 📖	mathematical	HasSum Pi.addCommMonoid Matrix Matrix.addCommMonoid Pi.topologicalSpace instTopologicalSpaceMatrix	HasSum Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix Matrix.blockDiagonal AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	map AddMonoidHom.instAddMonoidHomClass Continuous.matrix_blockDiagonal continuous_id
matrix_blockDiagonal' 📖	mathematical	HasSum Pi.addCommMonoid Matrix Matrix.addCommMonoid Pi.topologicalSpace instTopologicalSpaceMatrix	HasSum Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix Matrix.blockDiagonal' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	map AddMonoidHom.instAddMonoidHomClass Continuous.matrix_blockDiagonal' continuous_id
matrix_conjTranspose 📖	mathematical	HasSum Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix	HasSum Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix Matrix.conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid	—	map AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass Continuous.matrix_conjTranspose continuous_id
matrix_diag 📖	mathematical	HasSum Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix	HasSum Pi.addCommMonoid Pi.topologicalSpace Matrix.diag	—	map AddMonoidHom.instAddMonoidHomClass continuous_matrix_diag
matrix_diagonal 📖	mathematical	HasSum Pi.addCommMonoid Pi.topologicalSpace	HasSum Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix Matrix.diagonal AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	map AddMonoidHom.instAddMonoidHomClass Continuous.matrix_diagonal continuous_id
matrix_transpose 📖	mathematical	HasSum Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix	HasSum Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix Matrix.transpose	—	map AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass Continuous.matrix_transpose continuous_id

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
blockDiagonal'_tsum 📖	mathematical	—	blockDiagonal' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid tsum Pi.addCommMonoid Matrix addCommMonoid Pi.topologicalSpace instTopologicalSpaceMatrix	—	Function.LeftInverse.map_tsum instT2SpaceMatrix AddMonoidHom.instAddMonoidHomClass Continuous.matrix_blockDiagonal' continuous_id Continuous.matrix_blockDiag' blockDiag'_blockDiagonal'
blockDiagonal_tsum 📖	mathematical	—	blockDiagonal AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid tsum Pi.addCommMonoid Matrix addCommMonoid Pi.topologicalSpace instTopologicalSpaceMatrix	—	Function.LeftInverse.map_tsum instT2SpaceMatrix AddMonoidHom.instAddMonoidHomClass Continuous.matrix_blockDiagonal continuous_id Continuous.matrix_blockDiag blockDiag_blockDiagonal
conjTranspose_tsum 📖	mathematical	—	conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid tsum Matrix addCommMonoid instTopologicalSpaceMatrix	—	Function.LeftInverse.map_tsum instT2SpaceMatrix AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass Continuous.matrix_conjTranspose continuous_id conjTranspose_conjTranspose
diagonal_tsum 📖	mathematical	—	diagonal AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid tsum Pi.addCommMonoid Pi.topologicalSpace Matrix addCommMonoid instTopologicalSpaceMatrix	—	Function.LeftInverse.map_tsum instT2SpaceMatrix AddMonoidHom.instAddMonoidHomClass Continuous.matrix_diagonal continuous_id continuous_matrix_diag diag_diagonal
topologicalRing 📖	mathematical	—	IsTopologicalRing Matrix instTopologicalSpaceMatrix nonUnitalNonAssocRing	—	instIsTopologicalSemiringMatrix IsTopologicalRing.toIsTopologicalSemiring instContinuousNegMatrix IsSemitopologicalRing.toContinuousNeg IsTopologicalRing.toIsSemitopologicalRing
transpose_tsum 📖	mathematical	—	transpose tsum Matrix addCommMonoid instTopologicalSpaceMatrix	—	Function.LeftInverse.map_tsum instT2SpaceMatrix AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass Continuous.matrix_transpose continuous_id transpose_transpose

Summable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
matrix_blockDiag 📖	mathematical	Summable Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix	Summable Pi.addCommMonoid Matrix Matrix.addCommMonoid Pi.topologicalSpace instTopologicalSpaceMatrix Matrix.blockDiag	—	HasSum.summable HasSum.matrix_blockDiag hasSum
matrix_blockDiag' 📖	mathematical	Summable Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix	Summable Pi.addCommMonoid Matrix Matrix.addCommMonoid Pi.topologicalSpace instTopologicalSpaceMatrix Matrix.blockDiag'	—	HasSum.summable HasSum.matrix_blockDiag' hasSum
matrix_blockDiagonal 📖	mathematical	Summable Pi.addCommMonoid Matrix Matrix.addCommMonoid Pi.topologicalSpace instTopologicalSpaceMatrix	Summable Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix Matrix.blockDiagonal AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	HasSum.summable HasSum.matrix_blockDiagonal hasSum
matrix_blockDiagonal' 📖	mathematical	Summable Pi.addCommMonoid Matrix Matrix.addCommMonoid Pi.topologicalSpace instTopologicalSpaceMatrix	Summable Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix Matrix.blockDiagonal' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	HasSum.summable HasSum.matrix_blockDiagonal' hasSum
matrix_conjTranspose 📖	mathematical	Summable Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix	Summable Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix Matrix.conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid	—	HasSum.summable HasSum.matrix_conjTranspose hasSum
matrix_diag 📖	mathematical	Summable Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix	Summable Pi.addCommMonoid Pi.topologicalSpace Matrix.diag	—	HasSum.summable HasSum.matrix_diag hasSum
matrix_diagonal 📖	mathematical	Summable Pi.addCommMonoid Pi.topologicalSpace	Summable Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix Matrix.diagonal AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	HasSum.summable HasSum.matrix_diagonal hasSum
matrix_transpose 📖	mathematical	Summable Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix	Summable Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix Matrix.transpose	—	HasSum.summable HasSum.matrix_transpose hasSum

Topology.IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
matrix_map 📖	mathematical	Topology.IsClosedEmbedding	Topology.IsClosedEmbedding Matrix instTopologicalSpaceMatrix Matrix.map	—	piMap

Topology.IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
matrix_map 📖	mathematical	Topology.IsEmbedding	Topology.IsEmbedding Matrix instTopologicalSpaceMatrix Matrix.map	—	piMap

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
matrix_map 📖	mathematical	Topology.IsInducing	Topology.IsInducing Matrix instTopologicalSpaceMatrix Matrix.map	—	piMap

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
matrix_map 📖	mathematical	Topology.IsOpenEmbedding	Topology.IsOpenEmbedding Matrix instTopologicalSpaceMatrix Matrix.map	—	piMap

(root)

Definitions

Name	Category	Theorems
instTopologicalSpaceMatrix 📖	CompOp	106 math math: Matrix.IsSymm.exp, Matrix.IsHermitian.isClosedEmbedding_cfcAux, Continuous.matrix_blockDiag, Matrix.SpecialLinearGroup.continuous_toGL, Matrix.IsHermitian.det_abs, UpperHalfPlane.instContinuousSMulGL2R, Matrix.IsHermitian.cfc_eq, instContinuousStarMatrix, HasSum.matrix_conjTranspose, summable_matrix_transpose, Matrix.blockDiagonal_tsum, Matrix.exp_conj', Matrix.exp_neg, Summable.matrix_blockDiagonal, Summable.matrix_blockDiag, Continuous.matrix_conjTranspose, Continuous.matrix_replicateCol, instDiscreteTopologyMatrixOfFinite, Continuous.matrix_adjugate, Matrix.SpecialLinearGroup.isClosedEmbedding_toGL, HasSum.matrix_blockDiagonal', Matrix.exp_add_of_commute, Matrix.PosSemidef.det_sqrt, Matrix.conjTranspose_tsum, Matrix.IsHermitian.charpoly_cfc_eq, Matrix.GeneralLinearGroup.continuous_det, continuous_matrix, summable_matrix_diagonal, Matrix.IsHermitian.exp, Continuous.matrix_vecMulVec, Summable.matrix_diagonal, Matrix.exp_diagonal, HasSum.matrix_blockDiag', Summable.matrix_blockDiagonal', Matrix.exp_nsmul, Matrix.SpecialLinearGroup.isClosedEmbedding_mapGLInt, summable_matrix_conjTranspose, Matrix.exp_zsmul, instContinuousMulMatrixOfContinuousAdd, Matrix.exp_sum_of_commute, Matrix.SpecialLinearGroup.isInducing_mapGL, instContinuousConstSMulMatrix, continuousAt_matrix_inv, Matrix.GeneralLinearGroup.continuous_upperRightHom, summable_matrix_blockDiagonal', Continuous.matrix_mul, Matrix.exp_conjTranspose, Summable.matrix_blockDiag', HasSum.matrix_diagonal, Matrix.exp_transpose, CStarMatrix.ofMatrix_eq_ofMatrixL, Continuous.matrix_map, Continuous.matrix_updateCol, instContinuousAddMatrix, Continuous.matrix_blockDiagonal, Matrix.SpecialLinearGroup.isEmbedding_toGL, Continuous.matrix_replicateRow, Matrix.SpecialLinearGroup.isClosedEmbedding_val, continuous_matrix_diag, Matrix.exp_conj, Module.Basis.continuous_toMatrix, Matrix.IsHermitian.instContinuousFunctionalCalculusIsClosedEmbedding, Matrix.PosSemidef.inv_sqrt, Matrix.IsHermitian.cfcHom_eq_cfcAux, instIsTopologicalAddGroupMatrix, Continuous.matrix_blockDiag', Matrix.exp_blockDiagonal, Matrix.transpose_tsum, HasSum.matrix_blockDiag, Matrix.exp_units_conj', Topology.IsInducing.matrix_map, Continuous.matrix_diagonal, Summable.matrix_transpose, Summable.matrix_conjTranspose, instContinuousNegMatrix, instIsTopologicalSemiringMatrix, Topology.IsOpenEmbedding.matrix_map, Topology.IsEmbedding.matrix_map, Continuous.matrix_reindex, Matrix.topologicalRing, Continuous.matrix_fromBlocks, IsCompact.matrix, Matrix.isUnit_exp, Continuous.matrix_transpose, instT2SpaceMatrix, Matrix.SpecialLinearGroup.discreteSpecialLinearGroupIntRange, Matrix.exp_blockDiagonal', Matrix.diagonal_tsum, HasSum.matrix_blockDiagonal, Continuous.matrix_blockDiagonal', UpperHalfPlane.σ_eventuallyEq, HasSum.matrix_transpose, Matrix.blockDiagonal'_tsum, Matrix.exp_units_conj, Matrix.SpecialLinearGroup.isInducing_toGL, Continuous.matrix_submatrix, Subgroup.IsArithmetic.discreteTopology, Topology.IsClosedEmbedding.matrix_map, Matrix.PosDef.posDef_sqrt, instContinuousSMulMatrix, Matrix.IsHermitian.instContinuousFunctionalCalculus, IsOpen.matrix, instDiscreteTopologySubtypeGeneralLinearGroupMemSubgroupAdjoinNegOneOfIsTopologicalRingOfT2Space, summable_matrix_blockDiagonal, Matrix.SpecialLinearGroup.isEmbedding_mapGL, Continuous.matrix_updateRow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousAt_matrix_inv 📖	mathematical	ContinuousAt Ring.inverse Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Matrix.det	ContinuousAt Matrix instTopologicalSpaceMatrix Matrix.inv	—	ContinuousAt.smul instContinuousSMulMatrix ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring ContinuousAt.comp Continuous.continuousAt Continuous.matrix_det continuous_id Continuous.matrix_adjugate
continuous_matrix 📖	mathematical	Continuous	Continuous Matrix instTopologicalSpaceMatrix	—	continuous_pi
continuous_matrix_diag 📖	mathematical	—	Continuous Matrix instTopologicalSpaceMatrix Pi.topologicalSpace Matrix.diag	—	Continuous.matrix_diag continuous_id
instContinuousAddMatrix 📖	mathematical	—	ContinuousAdd Matrix instTopologicalSpaceMatrix Matrix.add	—	Pi.continuousAdd Pi.continuousAdd'
instContinuousConstSMulMatrix 📖	mathematical	—	ContinuousConstSMul Matrix instTopologicalSpaceMatrix Matrix.smul	—	—
instContinuousMulMatrixOfContinuousAdd 📖	mathematical	—	ContinuousMul Matrix instTopologicalSpaceMatrix Matrix.instMulOfFintypeOfAddCommMonoid	—	Continuous.matrix_mul continuous_fst continuous_snd
instContinuousNegMatrix 📖	mathematical	—	ContinuousNeg Matrix instTopologicalSpaceMatrix Matrix.neg	—	Pi.continuousNeg Pi.has_continuous_neg'
instContinuousSMulMatrix 📖	mathematical	—	ContinuousSMul Matrix Matrix.smul instTopologicalSpaceMatrix	—	—
instContinuousStarMatrix 📖	mathematical	—	ContinuousStar Matrix instTopologicalSpaceMatrix Matrix.instStar	—	Continuous.matrix_conjTranspose continuous_id
instDiscreteTopologyMatrixOfFinite 📖	mathematical	—	DiscreteTopology Matrix instTopologicalSpaceMatrix	—	—
instIsTopologicalAddGroupMatrix 📖	mathematical	—	IsTopologicalAddGroup Matrix instTopologicalSpaceMatrix Matrix.addGroup	—	Pi.topologicalAddGroup
instIsTopologicalSemiringMatrix 📖	mathematical	—	IsTopologicalSemiring Matrix instTopologicalSpaceMatrix Matrix.nonUnitalNonAssocSemiring	—	instContinuousAddMatrix IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring instContinuousMulMatrixOfContinuousAdd IsTopologicalSemiring.toContinuousMul
instT2SpaceMatrix 📖	mathematical	—	T2Space Matrix instTopologicalSpaceMatrix	—	—
summable_matrix_blockDiagonal 📖	mathematical	—	Summable Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix Matrix.blockDiagonal AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Pi.addCommMonoid Pi.topologicalSpace	—	Summable.map_iff_of_leftInverse AddMonoidHom.instAddMonoidHomClass Continuous.matrix_blockDiagonal continuous_id Continuous.matrix_blockDiag Matrix.blockDiag_blockDiagonal
summable_matrix_blockDiagonal' 📖	mathematical	—	Summable Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix Matrix.blockDiagonal' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Pi.addCommMonoid Pi.topologicalSpace	—	Summable.map_iff_of_leftInverse AddMonoidHom.instAddMonoidHomClass Continuous.matrix_blockDiagonal' continuous_id Continuous.matrix_blockDiag' Matrix.blockDiag'_blockDiagonal'
summable_matrix_conjTranspose 📖	mathematical	—	Summable Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix Matrix.conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid	—	Summable.map_iff_of_equiv AddEquiv.instAddEquivClass Continuous.matrix_conjTranspose continuous_id
summable_matrix_diagonal 📖	mathematical	—	Summable Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix Matrix.diagonal AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Pi.addCommMonoid Pi.topologicalSpace	—	Summable.map_iff_of_leftInverse AddMonoidHom.instAddMonoidHomClass Continuous.matrix_diagonal continuous_id continuous_matrix_diag Matrix.diag_diagonal
summable_matrix_transpose 📖	mathematical	—	Summable Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix Matrix.transpose	—	Summable.map_iff_of_equiv AddEquiv.instAddEquivClass Continuous.matrix_transpose continuous_id

---

← Back to Index