Theorem SeparatingDual.exists_separating_of_ne

Modification history

2023-08-11 14:14
Mathlib/Analysis/NormedSpace/HahnBanach/SeparatingDual.lean
feat: continuous linear equivalences act transitively on nonzero vectors (#6346) …
Added SeparatingDual.exists_separating_of_neView on Github →