Theorem coord_norm'

Modification history

2026-02-10 23:11

Mathlib/Analysis/Normed/Module/HahnBanach.lean

feat(Analysis/Normed/Module/{HahnBanach, Dual}): Weaken [NormedAddCommGroup] to seminormed (#34585) …

Deleted coord_norm'View on Github →

2023-05-24 09:36

Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean

feat: port Analysis.NormedSpace.HahnBanach.Extension (#4268)

Added coord_norm'View on Github →