Documentation Verification Report

Matrix

📁 Source: Mathlib/Topology/Algebra/Group/Matrix.lean

Statistics

Metric	Count
Definitions `instTopologicalSpace`	1
Theorems `continuous_det`, `continuous_upperRightHom`, `continuous_toGL`, `instDiscreteTopology`, `isClosedEmbedding_toGL`, `isClosedEmbedding_val`, `isEmbedding_mapGL`, `isEmbedding_toGL`, `isInducing_mapGL`, `isInducing_toGL`, `range_toGL`, `topologicalGroup`	12
Total	13

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` `IsSemitopologicalRing.toContinuousNeg` `IsTopologicalRing.toIsSemitopologicalRing`

Matrix.SpecialLinearGroup

Definitions

Name	Category	Theorems
`instTopologicalSpace` 📖	CompOp	13 math math: `continuous_toGL`, `topologicalGroup`, `isClosedEmbedding_toGL`, `instDiscreteTopology`, `UpperHalfPlane.isProperMap_smul_I`, `isClosedEmbedding_mapGLInt`, `isInducing_mapGL`, `UpperHalfPlane.instProperSMul`, `isEmbedding_toGL`, `UpperHalfPlane.continuous_toSL2R`, `UpperHalfPlane.instContinuousSMulSL2R`, `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`	—	—
`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` `IsSemitopologicalRing.toIsTopologicalAddGroup` `IsTopologicalRing.toIsSemitopologicalRing`
`isClosedEmbedding_val` 📖	mathematical	—	`Topology.IsClosedEmbedding` `Matrix` `Matrix.det` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instTopologicalSpaceSubtype` `instTopologicalSpaceMatrix`	—	`IsClosed.isClosedEmbedding_subtypeVal` `IsClosed.preimage` `Continuous.matrix_det` `continuous_id` `isClosed_singleton`
`isEmbedding_mapGL` 📖	mathematical	`Topology.IsEmbedding` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap`	`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` `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`	`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` `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` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `Continuous.comp` `continuous_induced_dom` `continuous_fst` `continuous_snd` `Continuous.matrix_adjugate`

---

← Back to Index