Documentation Verification Report

FiniteDimension

📁 Source: Mathlib/Topology/Algebra/Module/FiniteDimension.lean

Statistics

Metric	Count
Definitions `ofFinrankEq`, `toContinuousLinearEquivOfDetNeZero`, `toContinuousLinearEquiv`, `toContinuousLinearMap`, `constrL`, `equivFunL`, `toContinuousLinearMap`	7
Theorems `coe_toContinuousLinearEquivOfDetNeZero`, `exists_right_inverse_of_surjective`, `finiteDimensional`, `instModuleFinite`, `toContinuousLinearEquivOfDetNeZero_apply`, `toLinearMap_eq_iff_eq_toContinuousLinearMap`, `complete`, `nonempty_continuousLinearEquiv_iff_finrank_eq`, `nonempty_continuousLinearEquiv_of_finrank_eq`, `canLiftContinuousLinearEquiv`, `coe_toContinuousLinearEquiv`, `coe_toContinuousLinearEquiv'`, `coe_toContinuousLinearEquiv_symm`, `coe_toContinuousLinearEquiv_symm'`, `toLinearEquiv_toContinuousLinearEquiv`, `toLinearEquiv_toContinuousLinearEquiv_symm`, `canLiftContinuousLinearMap`, `coe_toContinuousLinearMap`, `coe_toContinuousLinearMap'`, `coe_toContinuousLinearMap_symm`, `continuousLinearMapClassOfFiniteDimensional`, `continuous_iff_isClosed_ker`, `continuous_of_finiteDimensional`, `continuous_of_isClosed_ker`, `continuous_of_nonzero_on_open`, `det_toContinuousLinearMap`, `isClosedEmbedding_of_injective`, `isOpenMap_of_finiteDimensional`, `ker_toContinuousLinearMap`, `range_toContinuousLinearMap`, `toContinuousLinearMap_eq_iff_eq_toLinearMap`, `of_finiteDimensional_of_complete`, `toLin_finTwoProd_toContinuousLinearMap`, `coe_constrL`, `constrL_apply`, `constrL_basis`, `equivFunL_apply`, `equivFunL_symm_apply_repr`, `closed_of_finiteDimensional`, `complete_of_finiteDimensional`, `continuous_equivFun_basis`, `isClosedEmbedding_smul_left`, `isClosedMap_smul_left`, `isModuleTopologyOfFiniteDimensional`, `unique_topology_of_t2`	45
Total	52

ContinuousLinearEquiv

Definitions

Name	Category	Theorems
`ofFinrankEq` 📖	CompOp	—

ContinuousLinearMap

Definitions

Name	Category	Theorems
`toContinuousLinearEquivOfDetNeZero` 📖	CompOp	2 math math: `coe_toContinuousLinearEquivOfDetNeZero`, `toContinuousLinearEquivOfDetNeZero_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toContinuousLinearEquivOfDetNeZero` 📖	mathematical	—	`ContinuousLinearEquiv.toContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `toContinuousLinearEquivOfDetNeZero`	—	`ext` `RingHomInvPair.ids`
`exists_right_inverse_of_surjective` 📖	mathematical	`LinearMap.range` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `toLinearMap` `Top.top` `Submodule` `Submodule.instTop`	`comp` `RingHomCompTriple.ids` `id`	—	`RingHomSurjective.ids` `RingHomCompTriple.ids` `LinearMap.exists_rightInverse_of_surjective` `Module.Projective.of_free` `Module.Free.of_divisionRing` `RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul`
`finiteDimensional` 📖	mathematical	—	`FiniteDimensional` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Field.toDivisionRing` `addCommGroup` `DivisionRing.toRing` `module` `DivisionRing.toDivisionSemiring` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing`	—	`smulCommClass_self` `instModuleFinite` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule`
`instModuleFinite` 📖	mathematical	—	`Module.Finite` `ContinuousLinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing`	—	`Module.Finite.of_injective` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `isNoetherian_linearMap` `coe_injective`
`toContinuousLinearEquivOfDetNeZero_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `toContinuousLinearEquivOfDetNeZero` `ContinuousLinearMap` `funLike`	—	`RingHomInvPair.ids`
`toLinearMap_eq_iff_eq_toContinuousLinearMap` 📖	mathematical	—	`toLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `LinearEquiv` `RingHomInvPair.ids` `LinearMap` `ContinuousLinearMap` `LinearMap.addCommMonoid` `addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `module` `ContinuousSMul.continuousConstSMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearMap.toContinuousLinearMap`	—	`RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul`

FiniteDimensional

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`complete` 📖	mathematical	—	`CompleteSpace`	—	`RingHomInvPair.ids` `IsUniformAddGroup.to_topologicalAddGroup` `Pi.topologicalAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instContinuousSMulForall` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Pi.t2Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `finiteDimensional_pi'` `Finite.of_fintype` `finiteDimensional_self` `Module.finrank_fin_fun` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `ContinuousLinearEquiv.isUniformEmbedding` `Pi.instIsUniformAddGroup` `SeminormedAddCommGroup.to_isUniformAddGroup` `completeSpace_congr` `Pi.complete`
`nonempty_continuousLinearEquiv_iff_finrank_eq` 📖	mathematical	—	`ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Module.finrank`	—	`RingHomInvPair.ids` `LinearEquiv.finrank_eq` `nonempty_continuousLinearEquiv_of_finrank_eq`
`nonempty_continuousLinearEquiv_of_finrank_eq` 📖	mathematical	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid`	`ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids`	—	`Nonempty.map` `RingHomInvPair.ids` `nonempty_linearEquiv_of_finrank_eq` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.of_divisionRing`

LinearEquiv

Definitions

Name	Category	Theorems
`toContinuousLinearEquiv` 📖	CompOp	6 math math: `toLinearEquiv_toContinuousLinearEquiv_symm`, `coe_toContinuousLinearEquiv_symm`, `coe_toContinuousLinearEquiv'`, `coe_toContinuousLinearEquiv_symm'`, `toLinearEquiv_toContinuousLinearEquiv`, `coe_toContinuousLinearEquiv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`canLiftContinuousLinearEquiv` 📖	mathematical	—	`CanLift` `LinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `ContinuousLinearEquiv` `ContinuousLinearEquiv.toLinearEquiv`	—	`RingHomInvPair.ids` `toLinearEquiv_toContinuousLinearEquiv`
`coe_toContinuousLinearEquiv` 📖	mathematical	—	`ContinuousLinearMap.toLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `toContinuousLinearEquiv` `toLinearMap`	—	`RingHomInvPair.ids`
`coe_toContinuousLinearEquiv'` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `toContinuousLinearEquiv` `LinearEquiv` `DFinsupp.instEquivLikeLinearEquiv`	—	`RingHomInvPair.ids`
`coe_toContinuousLinearEquiv_symm` 📖	mathematical	—	`ContinuousLinearMap.toLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `ContinuousLinearEquiv.symm` `toContinuousLinearEquiv` `toLinearMap` `symm`	—	`RingHomInvPair.ids`
`coe_toContinuousLinearEquiv_symm'` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `ContinuousLinearEquiv.symm` `toContinuousLinearEquiv` `LinearEquiv` `DFinsupp.instEquivLikeLinearEquiv` `symm`	—	`RingHomInvPair.ids`
`toLinearEquiv_toContinuousLinearEquiv` 📖	mathematical	—	`ContinuousLinearEquiv.toLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `toContinuousLinearEquiv`	—	`RingHomInvPair.ids` `ext`
`toLinearEquiv_toContinuousLinearEquiv_symm` 📖	mathematical	—	`ContinuousLinearEquiv.toLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `ContinuousLinearEquiv.symm` `toContinuousLinearEquiv` `symm`	—	`RingHomInvPair.ids` `ext`

LinearMap

Definitions

Name	Category	Theorems
`toContinuousLinearMap` 📖	CompOp	17 math math: `det_toContinuousLinearMap`, `adjoint_eq_toCLM_adjoint`, `isSelfAdjoint_toContinuousLinearMap_iff`, `coe_toContinuousLinearMap'`, `adjoint_toContinuousLinearMap`, `range_toContinuousLinearMap`, `Orientation.areaForm'_apply`, `coe_toContinuousLinearMap`, `toContinuousLinearMap_eq_iff_eq_toLinearMap`, `isPositive_toContinuousLinearMap_iff`, `ContinuousLinearMap.toLinearMap_eq_iff_eq_toContinuousLinearMap`, `Matrix.l2_opNNNorm_def`, `Matrix.toLin_finTwoProd_toContinuousLinearMap`, `isStarProjection_toContinuousLinearMap_iff`, `coe_toContinuousLinearMap_symm`, `Matrix.l2_opNorm_def`, `ker_toContinuousLinearMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`canLiftContinuousLinearMap` 📖	mathematical	—	`CanLift` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap` `ContinuousLinearMap.toLinearMap`	—	`RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul`
`coe_toContinuousLinearMap` 📖	mathematical	—	`ContinuousLinearMap.toLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `LinearEquiv` `RingHomInvPair.ids` `LinearMap` `ContinuousLinearMap` `addCommMonoid` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `ContinuousLinearMap.module` `ContinuousSMul.continuousConstSMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toContinuousLinearMap`	—	`RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul`
`coe_toContinuousLinearMap'` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `LinearEquiv` `RingHomInvPair.ids` `LinearMap` `addCommMonoid` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `ContinuousLinearMap.module` `ContinuousSMul.continuousConstSMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toContinuousLinearMap` `instFunLike`	—	`RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul`
`coe_toContinuousLinearMap_symm` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `ContinuousLinearMap` `AddCommGroup.toAddCommMonoid` `LinearMap` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `addCommMonoid` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `ContinuousSMul.continuousConstSMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.symm` `toContinuousLinearMap` `ContinuousLinearMap.toLinearMap`	—	`RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul`
`continuousLinearMapClassOfFiniteDimensional` 📖	mathematical	—	`ContinuousLinearMapClass` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike`	—	`semilinearMapClass` `continuous_of_finiteDimensional`
`continuous_iff_isClosed_ker` 📖	mathematical	—	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `instFunLike` `IsClosed` `SetLike.coe` `Submodule` `Submodule.setLike` `ker`	—	`IsClosed.preimage` `isClosed_singleton` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `continuous_of_isClosed_ker`
`continuous_of_finiteDimensional` 📖	mathematical	—	`Continuous` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike`	—	`IsModuleTopology.continuous_of_linearMap` `isModuleTopologyOfFiniteDimensional` `IsTopologicalAddGroup.toContinuousAdd`
`continuous_of_isClosed_ker` 📖	mathematical	—	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `instFunLike`	—	`RingHomSurjective.ids` `range_eq_bot` `Submodule.finrank_eq_zero` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `FiniteDimensional.finiteDimensional_submodule` `FiniteDimensional.finiteDimensional_self` `continuous_zero` `le_antisymm` `Submodule.finrank_le` `Module.finrank_self` `zero_lt_iff` `le_refl` `ker_eq_bot` `Submodule.ker_liftQ_eq_bot` `range_eq_top` `Submodule.range_liftQ` `Submodule.eq_top_of_finrank_eq` `RingHomInvPair.ids` `unique_topology_of_t2` `topologicalAddGroup_induced` `Submodule.topologicalAddGroup_quotient` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass` `continuousSMul_induced` `Submodule.continuousSMul_quotient` `instMulActionSemiHomClassMulActionHom` `t2Space_iff` `separated_by_continuous` `T25Space.t2Space` `T3Space.t25Space` `Submodule.t3_quotient_of_isClosed` `continuous_induced_dom` `Equiv.injective` `Equiv.induced_symm` `continuous_coinduced_rng` `Continuous.comp`
`continuous_of_nonzero_on_open` 📖	mathematical	`IsOpen` `Set.Nonempty`	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `instFunLike`	—	`continuous_of_isClosed_ker` `isClosed_or_dense_ker` `IsTopologicalAddGroup.toContinuousAdd` `instIsSimpleModule` `mem_interior_iff_mem_nhds` `Filter.mem_of_superset` `IsOpen.mem_nhds` `Dense.interior_compl`
`det_toContinuousLinearMap` 📖	mathematical	—	`ContinuousLinearMap.det` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DFunLike.coe` `LinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap` `addCommMonoid` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `ContinuousLinearMap.module` `ContinuousSMul.continuousConstSMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toContinuousLinearMap` `MonoidHom` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring` `MonoidHom.instFunLike` `det`	—	`RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul`
`isClosedEmbedding_of_injective` 📖	mathematical	`ker` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `Bot.bot` `Submodule` `Submodule.instBot`	`Topology.IsClosedEmbedding` `DFunLike.coe` `LinearMap` `instFunLike`	—	`RingHomInvPair.ids` `RingHomSurjective.invPair` `ker_eq_bot` `Submodule.topologicalAddGroup` `SMulMemClass.continuousSMul` `Submodule.smulMemClass` `instT2SpaceSubtype` `Topology.IsEmbedding.comp` `Topology.IsEmbedding.subtypeVal` `Homeomorph.isEmbedding` `Submodule.closed_of_finiteDimensional` `RingHomSurjective.ids` `finiteDimensional_range`
`isOpenMap_of_finiteDimensional` 📖	mathematical	`DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike`	`IsOpenMap`	—	`IsModuleTopology.isOpenMap_of_surjective` `isModuleTopologyOfFiniteDimensional` `IsTopologicalAddGroup.toContinuousAdd`
`ker_toContinuousLinearMap` 📖	mathematical	—	`ker` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousLinearMap.toLinearMap` `DFunLike.coe` `LinearEquiv` `RingHomInvPair.ids` `LinearMap` `ContinuousLinearMap` `addCommMonoid` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `ContinuousLinearMap.module` `ContinuousSMul.continuousConstSMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toContinuousLinearMap`	—	—
`range_toContinuousLinearMap` 📖	mathematical	—	`range` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `ContinuousLinearMap.toLinearMap` `DFunLike.coe` `LinearEquiv` `RingHomInvPair.ids` `LinearMap` `ContinuousLinearMap` `addCommMonoid` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `ContinuousLinearMap.module` `ContinuousSMul.continuousConstSMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toContinuousLinearMap`	—	`RingHomSurjective.ids` `RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul`
`toContinuousLinearMap_eq_iff_eq_toLinearMap` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap` `addCommMonoid` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `ContinuousLinearMap.module` `ContinuousSMul.continuousConstSMul` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toContinuousLinearMap` `ContinuousLinearMap.toLinearMap`	—	`RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul`

LocallyCompactSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_finiteDimensional_of_complete` 📖	mathematical	—	`LocallyCompactSpace`	—	`ContinuousSMul.continuousConstSMul` `Module.Basis.exists_basis` `SeparationQuotient.instModuleFinite` `Topology.IsOpenEmbedding.locallyCompactSpace` `Function.locallyCompactSpace_of_finite` `Finite.of_fintype` `RingHomInvPair.ids` `SeparationQuotient.instIsTopologicalAddGroup` `SeparationQuotient.instContinuousSMul` `Pi.topologicalAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instContinuousSMulForall` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeparationQuotient.t2Space` `instR1Space` `IsTopologicalAddGroup.regularSpace` `Pi.t2Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Homeomorph.isOpenEmbedding` `Topology.IsInducing.locallyCompactSpace` `IsClosed.isLocallyClosed` `isClosed_univ`

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toLin_finTwoProd_toContinuousLinearMap` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `AddCommGroup.toAddCommMonoid` `Prod.instAddCommGroup` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Prod.instModule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `ContinuousLinearMap` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `LinearMap.addCommMonoid` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `AddCommGroup.toAddGroup` `Prod.instIsTopologicalAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `ContinuousLinearMap.module` `ContinuousSMul.continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Prod.continuousSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `IsModuleTopology.toContinuousSMul` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `isModuleTopologyOfFiniteDimensional` `NormedSpace.toModule` `NormedField.toNormedSpace` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `MetricSpace.toEMetricSpace` `NormedField.toMetricSpace` `FiniteDimensional.finiteDimensional_self` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearMap.toContinuousLinearMap` `Prod.t2Space` `Module.IsNoetherian.finite` `DivisionRing.toDivisionSemiring` `isNoetherian_prod` `NormedRing.toRing` `NormedCommRing.toNormedRing` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Matrix` `Prod.instAddCommMonoid` `addCommMonoid` `module` `CommSemiring.toCommMonoid` `toLin` `Fin.fintype` `Finite.of_fintype` `Module.Basis.finTwoProd` `Equiv` `Equiv.instEquivLike` `of` `vecCons` `vecEmpty` `ContinuousLinearMap.prod` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.add` `IsTopologicalSemiring.toContinuousAdd` `ContinuousLinearMap.instSMul` `NonUnitalNonAssocSemiring.toDistribSMul` `Algebra.to_smulCommClass` `Algebra.id` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ContinuousLinearMap.fst` `ContinuousLinearMap.snd`	—	`ContinuousLinearMap.ext` `RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousAdd` `Prod.instIsTopologicalAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `Prod.continuousSMul` `IsModuleTopology.toContinuousSMul` `isModuleTopologyOfFiniteDimensional` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `FiniteDimensional.finiteDimensional_self` `Prod.t2Space` `Module.IsNoetherian.finite` `isNoetherian_prod` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `Finite.of_fintype` `IsTopologicalSemiring.toContinuousAdd` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `SeminormedAddCommGroup.to_isUniformAddGroup` `IsTopologicalSemiring.toContinuousMul` `toLin_finTwoProd_apply`

Module.Basis

Definitions

Name	Category	Theorems
`constrL` 📖	CompOp	3 math math: `constrL_basis`, `constrL_apply`, `coe_constrL`
`equivFunL` 📖	CompOp	6 math math: `NumberField.mixedEmbedding.fundamentalCone.abs_det_completeBasis_equivFunL_symm`, `equivFunL_symm_apply_repr`, `equivFunL_apply`, `parallelepiped_eq_map`, `opNNNorm_le`, `opNorm_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_constrL` 📖	mathematical	—	`ContinuousLinearMap.toLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `constrL` `DFunLike.coe` `LinearEquiv` `RingHomInvPair.ids` `LinearMap` `Pi.addCommMonoid` `LinearMap.addCommMonoid` `Pi.Function.module` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `constr`	—	—
`constrL_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `constrL` `Finite.of_fintype` `Finset.sum` `Finset.univ` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `LinearEquiv` `RingHomInvPair.ids` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `equivFun`	—	`constr_apply_fintype`
`constrL_basis` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `constrL` `Module.Basis` `instFunLike`	—	`constr_basis`
`equivFunL_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Pi.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Pi.Function.module` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `equivFunL` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `LinearEquiv.instEquivLike` `repr`	—	`RingHomInvPair.ids`
`equivFunL_symm_apply_repr` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Pi.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `AddCommGroup.toAddCommMonoid` `Pi.Function.module` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `ContinuousLinearEquiv.symm` `equivFunL` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `DFinsupp.instEquivLikeLinearEquiv` `repr`	—	`ContinuousLinearEquiv.symm_apply_apply` `RingHomInvPair.ids`

Module.End

Definitions

Name	Category	Theorems
`toContinuousLinearMap` 📖	CompOp	—

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closed_of_finiteDimensional` 📖	mathematical	—	`IsClosed` `SetLike.coe` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid` `setLike`	—	`IsComplete.isClosed` `T1Space.t0Space` `T2Space.t1Space` `complete_of_finiteDimensional` `isUniformAddGroup_of_addCommGroup`
`complete_of_finiteDimensional` 📖	mathematical	—	`IsComplete` `SetLike.coe` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid` `setLike`	—	`completeSpace_coe_iff_isComplete` `FiniteDimensional.complete` `instT2SpaceSubtype` `AddSubgroup.isUniformAddGroup` `SMulMemClass.continuousSMul` `smulMemClass`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_equivFun_basis` 📖	mathematical	—	`Continuous` `Pi.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `DFunLike.coe` `LinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Module.Basis.equivFun`	—	`LinearMap.continuous_of_finiteDimensional` `Pi.topologicalAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instContinuousSMulForall` `IsModuleTopology.toContinuousSMul` `isModuleTopologyOfFiniteDimensional` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `FiniteDimensional.finiteDimensional_self` `Module.Basis.finiteDimensional_of_finite` `RingHomInvPair.ids`
`isClosedEmbedding_smul_left` 📖	mathematical	—	`Topology.IsClosedEmbedding` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`LinearMap.isClosedEmbedding_of_injective` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `FiniteDimensional.finiteDimensional_self` `LinearMap.ker_toSpanSingleton` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors`
`isClosedMap_smul_left` 📖	mathematical	—	`IsClosedMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`smul_zero` `isClosedMap_const` `T2Space.t1Space` `Topology.IsClosedEmbedding.isClosedMap` `isClosedEmbedding_smul_left`
`isModuleTopologyOfFiniteDimensional` 📖	mathematical	—	`IsModuleTopology` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction`	—	`RingHomInvPair.ids` `Finite.of_fintype` `IsModuleTopology.continuous_of_linearMap` `IsModuleTopology.instPi` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsTopologicalAddGroup.toContinuousAdd` `IsModuleTopology.iso`
`unique_topology_of_t2` 📖	mathematical	—	`UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `NormedField.toMetricSpace` `NontriviallyNormedField.toNormedField`	—	`IsTopologicalAddGroup.ext` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `le_antisymm` `Filter.HasBasis.ge_iff` `Metric.nhds_basis_closedBall` `NormedField.exists_norm_lt` `IsOpen.mem_nhds` `isOpen_compl_singleton` `T2Space.t1Space` `Set.mem_compl_singleton_iff` `norm_ne_zero_iff` `LT.lt.ne` `balancedCore_mem_nhds_zero` `NormedField.nhdsNE_neBot` `Filter.mem_of_superset` `Metric.mem_closedBall_self` `LT.lt.le` `mem_closedBall_zero_iff` `Balanced.smul_mem` `balancedCore_balanced` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_inv` `mul_inv_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `norm_pos_iff` `one_mul` `LT.lt.trans` `Set.notMem_compl_iff` `Set.mem_singleton` `balancedCore_subset` `mul_one` `inv_mul_cancel₀` `mul_assoc` `smul_eq_mul` `Filter.map_id` `Filter.Tendsto.smul_const` `Filter.tendsto_id` `zero_smul`

---

← Back to Index