Commit 2023-05-17 23:10 99e853dc

View on Github →

feat: port Topology.Algebra.Module.FiniteDimension (#3796)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/ModuleCat/Basic.lean

Modified Mathlib/Algebra/Module/LinearMap.lean

Created Mathlib/Topology/Algebra/Module/FiniteDimension.lean

added theorem Basis.coe_constrL

added def Basis.constrL

added theorem Basis.constrL_apply

added theorem Basis.constrL_basis

added def Basis.equivFunL

added def ContinuousLinearEquiv.ofFinrankEq

added theorem ContinuousLinearMap.coe_toContinuousLinearEquivOfDetNeZero

added def ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero

added theorem ContinuousLinearMap.toContinuousLinearEquivOfDetNeZero_apply

added theorem FiniteDimensional.nonempty_continuousLinearEquiv_iff_finrank_eq

added theorem FiniteDimensional.nonempty_continuousLinearEquiv_of_finrank_eq

added theorem LinearEquiv.coe_toContinuousLinearEquiv

added theorem LinearEquiv.coe_toContinuousLinearEquiv_symm'

added theorem LinearEquiv.coe_toContinuousLinearEquiv_symm

added theorem LinearEquiv.coe_to_continuous_linear_equiv'

added def LinearEquiv.toContinuousLinearEquiv

added theorem LinearEquiv.toLinearEquiv_toContinuousLinearEquiv

added theorem LinearEquiv.toLinearEquiv_toContinuousLinearEquiv_symm

added theorem LinearMap.coe_toContinuousLinearMap

added theorem LinearMap.coe_toContinuousLinearMap_symm

added theorem LinearMap.coe_to_continuous_linear_map'

added theorem LinearMap.continuous_iff_isClosed_ker

added theorem LinearMap.continuous_of_finiteDimensional

added theorem LinearMap.continuous_of_isClosed_ker

added theorem LinearMap.continuous_of_nonzero_on_open

added theorem LinearMap.det_toContinuousLinearMap

added theorem LinearMap.isOpenMap_of_finiteDimensional

added theorem LinearMap.ker_toContinuousLinearMap

added theorem LinearMap.range_toContinuousLinearMap

added def LinearMap.toContinuousLinearMap

added theorem Matrix.toLin_finTwoProd_toContinuousLinearMap

added theorem continuous_equivFun_basis

added theorem unique_topology_of_t2

Modified Mathlib/Topology/Algebra/UniformGroup.lean