Theorem abs_norm

Modification history

2024-02-05 06:26

Mathlib/Analysis/NormedSpace/Basic.lean

chore(Normed): move `abs_norm`, add `abs_norm'` (#10202)

Deleted abs_norm View on Github →

2023-05-06 08:29

Mathlib/Analysis/NormedSpace/Basic.lean

chore: fix names (#3812) …

Added abs_norm View on Github →