Theorem SeparatingDual.exists_continuousLinearEquiv_apply_eq

Modification history

2026-01-28 18:47

Mathlib/Analysis/LocallyConvex/SeparatingDual.lean

chore(Analysis/LocallyConvex/SeparatingDual): generalize `Algebra.IsCentral.instContinuousLinearMap` (#33351) …

Modified SeparatingDual.exists_continuousLinearEquiv_apply_eq View on Github →

2023-08-11 14:14

Mathlib/Analysis/NormedSpace/HahnBanach/SeparatingDual.lean

feat: continuous linear equivalences act transitively on nonzero vectors (#6346) …

Added SeparatingDual.exists_continuousLinearEquiv_apply_eq View on Github →