Commit 2023-12-03 09:54 6e7be968

View on Github →

feat(Analysis/HahnBanach): extension of a CLM with finite dimensional range (#8604) Also add 2 missing simp lemmas and prove that a finite dimensional subspace is ClosedComplemented.

Estimated changes

Modified Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean

added theorem ContinuousLinearMap.exist_extension_of_finiteDimensional_range

added theorem Submodule.ClosedComplemented.of_finiteDimensional

modified theorem exists_extension_norm_eq

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

added theorem Basis.equivFunL_symm_apply_repr