Theorem SeparatingDual.exists_ne_zero

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_ne_zeroView on Github →