ContinuousLinearMap

Statistics

Metric	Count
Definitions	0
Theorems `isClosed_eigenspace`, `isClosed_genEigenspace`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosed_eigenspace` 📖	mathematical	—	`IsClosed` `SetLike.coe` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.setLike` `Module.End.eigenspace` `toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring`	—	`isClosed_genEigenspace`
`isClosed_genEigenspace` 📖	mathematical	—	`IsClosed` `SetLike.coe` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.setLike` `DFunLike.coe` `OrderHom` `ENat` `instPreorderENat` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `OrderHom.instFunLike` `Module.End.genEigenspace` `toLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ENat.instNatCast`	—	`smulCommClass_self` `Module.End.genEigenspace_nat` `Module.End.one_eq_id` `coe_id` `coe_smul` `coe_sub` `coe_pow` `isClosed_ker` `T2Space.t1Space` `T25Space.t2Space` `T3Space.t25Space` `instT3Space` `IsTopologicalAddGroup.regularSpace`

---