Commit 2024-02-08 10:24 75ae8cbb
View on Github →chore(NormedSpace/FiniteDimension): reuse a proof about groups (#10313)
Reuse HasCompactSupport.eq_zero_or_locallyCompactSpace_of_addGroup
in the proof of HasCompactSupport.eq_zero_or_finiteDimensional.