Theorem Basis.equivFunL_symm_apply_repr

Modification history

2025-07-24 16:31
Mathlib/Topology/Algebra/Module/FiniteDimension.lean
chore: rename `Basis` to `Module.Basis` (#27381) …
Deleted Basis.equivFunL_symm_apply_reprView on Github →
2023-12-03 09:54
Mathlib/Topology/Algebra/Module/FiniteDimension.lean
feat(Analysis/HahnBanach): extension of a CLM with finite dimensional range (#8604) …
Added Basis.equivFunL_symm_apply_reprView on Github →