Commit 2023-09-05 10:32 6da24862

View on Github →

feat: generalize some lemmas from a normed space to a TVS (#5771)

Generalize FiniteDimensional.complete, Submodule.complete_of_finiteDimensional from a normed space over 𝕜 to a uniform additive commutative group that is a TVS over 𝕜.
Generalize Submodule.closed_of_finiteDimensional, LinearMap.closedEmbedding_of_injective, closedEmbedding_smul_left isClosedMap_smul_left, and ContinuousLinearMap.exists_right_inverse_of_surjective from a normed space to a TVS.
Rename finiteDimensional_of_isCompact_closed_ball₀ to finiteDimensional_of_isCompact_closedBall₀.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

Modified Mathlib/Analysis/NormedSpace/FiniteDimension.lean

deleted theorem ContinuousLinearMap.exists_right_inverse_of_surjective

deleted theorem FiniteDimensional.complete

deleted theorem LinearEquiv.closedEmbedding_of_injective

deleted theorem Submodule.closed_of_finiteDimensional

deleted theorem Submodule.complete_of_finiteDimensional

deleted theorem closedEmbedding_smul_left

added theorem finiteDimensional_of_isCompact_closedBall₀

deleted theorem finiteDimensional_of_isCompact_closed_ball₀

deleted theorem isClosedMap_smul_left

Modified Mathlib/NumberTheory/Modular.lean

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

added theorem ContinuousLinearMap.exists_right_inverse_of_surjective

added theorem FiniteDimensional.complete

added theorem LinearMap.closedEmbedding_of_injective

added theorem Submodule.closed_of_finiteDimensional

added theorem Submodule.complete_of_finiteDimensional

added theorem closedEmbedding_smul_left

added theorem isClosedMap_smul_left