Matrix

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

Statistics

Metric	Count
Definitions instTopologicalSpace, instTopologicalSpaceMatrix	2
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, continuous_det, continuous_upperRightHom, continuous_toGL, instDiscreteTopology, isClosedEmbedding_toGL, isEmbedding_mapGL, isEmbedding_toGL, isInducing_mapGL, isInducing_toGL, range_toGL, topologicalGroup, 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	81
Total	83

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dotProduct 📖	mathematical	Continuous Pi.topologicalSpace	dotProduct	—	continuous_finset_sum fun_mul comp' continuous_apply
matrix_adjugate 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Matrix.adjugate	—	continuous_matrix matrix_det matrix_updateCol matrix_transpose continuous_const
matrix_blockDiag 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Pi.topologicalSpace Matrix.blockDiag	—	continuous_pi continuous_matrix matrix_elem
matrix_blockDiag' 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Pi.topologicalSpace Matrix.blockDiag'	—	continuous_pi continuous_matrix matrix_elem
matrix_blockDiagonal 📖	mathematical	Continuous Pi.topologicalSpace Matrix instTopologicalSpaceMatrix	Matrix.blockDiagonal	—	continuous_matrix if_const matrix_elem comp continuous_apply continuous_zero
matrix_blockDiagonal' 📖	mathematical	Continuous Pi.topologicalSpace Matrix instTopologicalSpaceMatrix	Matrix.blockDiagonal'	—	continuous_matrix matrix_elem comp continuous_apply continuous_const
matrix_conjTranspose 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Matrix.conjTranspose	—	matrix_map matrix_transpose ContinuousStar.continuous_star
matrix_cramer 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix 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	Matrix.det	—	Matrix.det_apply continuous_finset_sum IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring const_smul Units.continuousConstSMul AddGroup.continuousConstSMul_int IsTopologicalRing.to_topologicalAddGroup continuous_finset_prod IsTopologicalSemiring.toContinuousMul matrix_elem
matrix_diag 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Pi.topologicalSpace Matrix.diag	—	continuous_pi matrix_elem
matrix_diagonal 📖	mathematical	Continuous Pi.topologicalSpace	Matrix instTopologicalSpaceMatrix Matrix.diagonal	—	continuous_matrix if_const comp continuous_apply continuous_zero
matrix_elem 📖	—	Continuous Matrix instTopologicalSpaceMatrix	—	—	comp continuous_apply_apply
matrix_fromBlocks 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Matrix.fromBlocks	—	continuous_matrix matrix_elem
matrix_map 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Matrix.map	—	continuous_matrix comp matrix_elem
matrix_mul 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Matrix.instHMulOfFintypeOfMulOfAddCommMonoid	—	continuous_matrix continuous_finset_sum mul matrix_elem
matrix_mulVec 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix Pi.topologicalSpace	Matrix.mulVec	—	continuous_pi dotProduct comp continuous_apply
matrix_reindex 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Matrix.reindex	—	matrix_submatrix
matrix_replicateCol 📖	mathematical	Continuous Pi.topologicalSpace	Matrix instTopologicalSpaceMatrix Matrix.replicateCol	—	continuous_matrix comp continuous_apply
matrix_replicateRow 📖	mathematical	Continuous Pi.topologicalSpace	Matrix instTopologicalSpaceMatrix Matrix.replicateRow	—	continuous_matrix comp continuous_apply
matrix_submatrix 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Matrix.submatrix	—	continuous_matrix matrix_elem
matrix_trace 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Matrix.trace	—	continuous_finset_sum matrix_elem
matrix_transpose 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix	Matrix.transpose	—	continuous_matrix matrix_elem
matrix_updateCol 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix Pi.topologicalSpace	Matrix.updateCol	—	continuous_matrix comp continuous_apply update
matrix_updateRow 📖	mathematical	Continuous Matrix instTopologicalSpaceMatrix Pi.topologicalSpace	Matrix.updateRow	—	update
matrix_vecMul 📖	mathematical	Continuous Pi.topologicalSpace Matrix instTopologicalSpaceMatrix	Matrix.vecMul	—	continuous_pi dotProduct matrix_elem
matrix_vecMulVec 📖	mathematical	Continuous Pi.topologicalSpace	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	Pi.addCommMonoid Pi.topologicalSpace Matrix.blockDiag	—	map AddMonoidHom.instAddMonoidHomClass Continuous.matrix_blockDiag continuous_id
matrix_blockDiag' 📖	mathematical	HasSum Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix	Pi.addCommMonoid Pi.topologicalSpace Matrix.blockDiag'	—	map AddMonoidHom.instAddMonoidHomClass Continuous.matrix_blockDiag' continuous_id
matrix_blockDiagonal 📖	mathematical	HasSum Pi.addCommMonoid Matrix Matrix.addCommMonoid Pi.topologicalSpace 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	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	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	Pi.addCommMonoid Pi.topologicalSpace Matrix.diag	—	map AddMonoidHom.instAddMonoidHomClass continuous_matrix_diag
matrix_diagonal 📖	mathematical	HasSum Pi.addCommMonoid Pi.topologicalSpace	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	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 IsTopologicalRing.toContinuousNeg
transpose_tsum 📖	mathematical	—	transpose tsum Matrix addCommMonoid instTopologicalSpaceMatrix	—	Function.LeftInverse.map_tsum instT2SpaceMatrix AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass Continuous.matrix_transpose continuous_id transpose_transpose

Matrix.GeneralLinearGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_det 📖	mathematical	—	Continuous Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Units.instTopologicalSpaceUnits Matrix instTopologicalSpaceMatrix Matrix.semiring DFunLike.coe MonoidHom MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike det	—	MonoidHom.instMonoidHomClass Continuous.matrix_det Units.continuous_val Units.continuous_coe_inv
continuous_upperRightHom 📖	mathematical	—	Continuous Matrix.GeneralLinearGroup Fin.fintype Ring.toSemiring Units.instTopologicalSpaceUnits Matrix instTopologicalSpaceMatrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring DFunLike.coe AddChar AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Units.instMonoid AddChar.instFunLike upperRightHom	—	continuous_matrix Fintype.complete Matrix.cons_val' Matrix.cons_val_fin_one IsTopologicalRing.toContinuousNeg

Matrix.SpecialLinearGroup

Definitions

Name	Category	Theorems
instTopologicalSpace 📖	CompOp	9 math math: continuous_toGL, topologicalGroup, isClosedEmbedding_toGL, instDiscreteTopology, isClosedEmbedding_mapGLInt, isInducing_mapGL, isEmbedding_toGL, isInducing_toGL, isEmbedding_mapGL

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_toGL 📖	mathematical	—	Continuous Matrix.SpecialLinearGroup Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring instTopologicalSpace Units.instTopologicalSpaceUnits Matrix instTopologicalSpaceMatrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass monoid Units.instMulOneClass MonoidHom.instFunLike toGL	—	MonoidHom.instMonoidHomClass continuous_subtype_val Continuous.comp' Continuous.inv IsTopologicalGroup.toContinuousInv topologicalGroup continuous_id'
instDiscreteTopology 📖	mathematical	—	DiscreteTopology Matrix.SpecialLinearGroup instTopologicalSpace	—	instDiscreteTopologySubtype instDiscreteTopologyMatrixOfFinite Finite.of_fintype
isClosedEmbedding_toGL 📖	mathematical	—	Topology.IsClosedEmbedding Matrix.SpecialLinearGroup Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring instTopologicalSpace Units.instTopologicalSpaceUnits Matrix instTopologicalSpaceMatrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass monoid Units.instMulOneClass MonoidHom.instFunLike toGL	—	isEmbedding_toGL range_toGL IsClosed.preimage Matrix.GeneralLinearGroup.continuous_det isClosed_singleton T2Space.t1Space Units.instT2Space T25Space.t2Space T3Space.t25Space instT3Space IsTopologicalAddGroup.regularSpace IsTopologicalRing.to_topologicalAddGroup
isEmbedding_mapGL 📖	mathematical	Topology.IsEmbedding DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	Matrix.SpecialLinearGroup Matrix.GeneralLinearGroup instTopologicalSpace Units.instTopologicalSpaceUnits Matrix instTopologicalSpaceMatrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass monoid Units.instMulOneClass MonoidHom.instFunLike mapGL	—	isInducing_mapGL Topology.IsEmbedding.isInducing mapGL_injective faithfulSMul_iff_algebraMap_injective Topology.IsEmbedding.injective
isEmbedding_toGL 📖	mathematical	—	Topology.IsEmbedding Matrix.SpecialLinearGroup Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring instTopologicalSpace Units.instTopologicalSpaceUnits Matrix instTopologicalSpaceMatrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass monoid Units.instMulOneClass MonoidHom.instFunLike toGL	—	isInducing_toGL toGL_injective
isInducing_mapGL 📖	mathematical	Topology.IsInducing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	Matrix.SpecialLinearGroup Matrix.GeneralLinearGroup instTopologicalSpace Units.instTopologicalSpaceUnits Matrix instTopologicalSpaceMatrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass monoid Units.instMulOneClass MonoidHom.instFunLike mapGL	—	Topology.IsInducing.comp isInducing_toGL Topology.IsInducing.of_comp continuous_induced_rng Continuous.matrix_map continuous_subtype_val Topology.IsInducing.continuous continuous_induced_dom Topology.IsInducing.matrix_map Topology.IsInducing.induced
isInducing_toGL 📖	mathematical	—	Topology.IsInducing Matrix.SpecialLinearGroup Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring instTopologicalSpace Units.instTopologicalSpaceUnits Matrix instTopologicalSpaceMatrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass monoid Units.instMulOneClass MonoidHom.instFunLike toGL	—	Topology.IsInducing.of_comp continuous_toGL Units.continuous_val Topology.IsInducing.induced
range_toGL 📖	mathematical	—	Set.range Matrix.GeneralLinearGroup CommSemiring.toSemiring CommRing.toCommSemiring Matrix.SpecialLinearGroup DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass monoid Units.instMulOneClass Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MonoidHom.instFunLike toGL Set.preimage Units Matrix.GeneralLinearGroup.det Set Set.instSingletonSet Units.instOne	—	Set.ext Matrix.det.congr_simp det_coe
topologicalGroup 📖	mathematical	—	IsTopologicalGroup Matrix.SpecialLinearGroup instTopologicalSpace instGroup	—	Continuous.mul instContinuousMulMatrixOfContinuousAdd IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalSemiring.toContinuousMul Continuous.comp continuous_induced_dom continuous_fst continuous_snd Continuous.matrix_adjugate

Summable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
matrix_blockDiag 📖	mathematical	Summable Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix	Pi.addCommMonoid Pi.topologicalSpace Matrix.blockDiag	—	HasSum.summable HasSum.matrix_blockDiag hasSum
matrix_blockDiag' 📖	mathematical	Summable Matrix Matrix.addCommMonoid instTopologicalSpaceMatrix	Pi.addCommMonoid Pi.topologicalSpace Matrix.blockDiag'	—	HasSum.summable HasSum.matrix_blockDiag' hasSum
matrix_blockDiagonal 📖	mathematical	Summable Pi.addCommMonoid Matrix Matrix.addCommMonoid Pi.topologicalSpace 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	Matrix.blockDiagonal' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	HasSum.summable HasSum.matrix_blockDiagonal' hasSum
matrix_conjTranspose 📖	mathematical	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	Pi.addCommMonoid Pi.topologicalSpace Matrix.diag	—	HasSum.summable HasSum.matrix_diag hasSum
matrix_diagonal 📖	mathematical	Summable Pi.addCommMonoid Pi.topologicalSpace	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	Matrix.transpose	—	HasSum.summable HasSum.matrix_transpose hasSum

Topology.IsClosedEmbedding

Theorems

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

Topology.IsEmbedding

Theorems

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

Topology.IsInducing

Theorems

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

Topology.IsOpenEmbedding

Theorems

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

(root)

Definitions

Name	Category	Theorems
instTopologicalSpaceMatrix 📖	CompOp	84 math math: Matrix.IsSymm.exp, Matrix.IsHermitian.isClosedEmbedding_cfcAux, Matrix.SpecialLinearGroup.continuous_toGL, Matrix.IsHermitian.det_abs, Matrix.IsHermitian.cfc_eq, instContinuousStarMatrix, summable_matrix_transpose, Matrix.PosSemidef.sqrt_eq_zero_iff, Matrix.blockDiagonal_tsum, Matrix.exp_conj', Matrix.exp_neg, Continuous.matrix_replicateCol, instDiscreteTopologyMatrixOfFinite, Matrix.SpecialLinearGroup.isClosedEmbedding_toGL, Matrix.exp_add_of_commute, Matrix.PosSemidef.det_sqrt, Matrix.conjTranspose_tsum, Matrix.IsHermitian.charpoly_cfc_eq, Matrix.GeneralLinearGroup.continuous_det, Matrix.PosSemidef.posSemidef_sqrt, continuous_matrix, summable_matrix_diagonal, Matrix.IsHermitian.exp, Matrix.PosSemidef.sqrt_eq_one_iff, Matrix.PosSemidef.sqrt_sq, Continuous.matrix_vecMulVec, Summable.matrix_diagonal, Matrix.PosSemidef.eq_sqrt_iff_sq_eq, Matrix.exp_diagonal, 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', Matrix.exp_conjTranspose, HasSum.matrix_diagonal, Matrix.exp_transpose, CStarMatrix.ofMatrix_eq_ofMatrixL, instContinuousAddMatrix, Matrix.PosSemidef.isUnit_sqrt_iff, Matrix.SpecialLinearGroup.isEmbedding_toGL, Continuous.matrix_replicateRow, continuous_matrix_diag, Matrix.exp_conj, Module.Basis.continuous_toMatrix, Matrix.PosSemidef.sq_sqrt, Matrix.PosSemidef.inv_sqrt, instIsTopologicalAddGroupMatrix, Matrix.exp_blockDiagonal, Matrix.transpose_tsum, Matrix.exp_units_conj', Topology.IsInducing.matrix_map, Continuous.matrix_diagonal, instContinuousNegMatrix, instIsTopologicalSemiringMatrix, Topology.IsOpenEmbedding.matrix_map, Topology.IsEmbedding.matrix_map, Matrix.topologicalRing, IsCompact.matrix, Matrix.isUnit_exp, instT2SpaceMatrix, Matrix.SpecialLinearGroup.discreteSpecialLinearGroupIntRange, Matrix.PosSemidef.sqrt_mul_self, Matrix.exp_blockDiagonal', Matrix.diagonal_tsum, Matrix.blockDiagonal'_tsum, Matrix.exp_units_conj, Matrix.SpecialLinearGroup.isInducing_toGL, Subgroup.IsArithmetic.discreteTopology, Topology.IsClosedEmbedding.matrix_map, Matrix.PosDef.posDef_sqrt, instContinuousSMulMatrix, Matrix.IsHermitian.instContinuousFunctionalCalculus, IsOpen.matrix, instDiscreteTopologySubtypeGeneralLinearGroupMemSubgroupAdjoinNegOneOfIsTopologicalRingOfT2Space, summable_matrix_blockDiagonal, Matrix.PosSemidef.sqrt_eq_iff_eq_sq, Matrix.SpecialLinearGroup.isEmbedding_mapGL

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousAt_matrix_inv 📖	mathematical	ContinuousAt Ring.inverse Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Matrix.det	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	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	—	instContinuousConstSMulForall
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	—	instContinuousSMulForall
instContinuousStarMatrix 📖	mathematical	—	ContinuousStar Matrix instTopologicalSpaceMatrix Matrix.instStar	—	Continuous.matrix_conjTranspose continuous_id
instDiscreteTopologyMatrixOfFinite 📖	mathematical	—	DiscreteTopology Matrix instTopologicalSpaceMatrix	—	Pi.discreteTopology
instIsTopologicalAddGroupMatrix 📖	mathematical	—	IsTopologicalAddGroup Matrix instTopologicalSpaceMatrix Matrix.addGroup	—	Pi.topologicalAddGroup
instIsTopologicalSemiringMatrix 📖	mathematical	—	IsTopologicalSemiring Matrix instTopologicalSpaceMatrix Matrix.nonUnitalNonAssocSemiring	—	instContinuousAddMatrix IsTopologicalSemiring.toContinuousAdd instContinuousMulMatrixOfContinuousAdd IsTopologicalSemiring.toContinuousMul
instT2SpaceMatrix 📖	mathematical	—	T2Space Matrix instTopologicalSpaceMatrix	—	Pi.t2Space
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