Theorem SeparatingDual.exists_eq_one_ne_zero_of_ne_zero_pair

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