Theorem ContinuousLinearEquiv.coord_norm'

Modification history

2026-02-10 23:11
Mathlib/Analysis/Normed/Module/RCLike/Basic.lean
feat(Analysis/Normed/Module/{HahnBanach, Dual}): Weaken [NormedAddCommGroup] to seminormed (#34585) …
Added ContinuousLinearEquiv.coord_norm'View on Github →