Theorem ContinuousLinearEquiv.conjContinuousAlgEquiv_ext_iff

Modification history

2026-02-10 19:29
Mathlib/Analysis/LocallyConvex/SeparatingDual.lean
feat: `{Continuous}Linear{Isometry}Equiv.conj{Continuous, Star}AlgEquiv` are "almost" injective (#33417) …
Added ContinuousLinearEquiv.conjContinuousAlgEquiv_ext_iffView on Github →