Theorem dist_one

Modification history

2025-02-03 06:56
Mathlib/Analysis/Normed/Group/Basic.lean
chore: replace the lemma that `dist 1 = norm` by `dist 1 a = ‖a‖` (#21340) …
Added dist_oneView on Github →