Theorem Inseparable.enorm_eq_enorm

Modification history

2026-01-14 14:17
Mathlib/Analysis/Normed/Group/Continuity.lean
feat(to_dual): linter for redundant uses of `to_dual`/`to_additive` (#33239) …
Added Inseparable.enorm_eq_enormView on Github →