Theorem dist_one_left

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) …

Modified dist_one_left View on Github →

2023-03-09 06:58

Mathlib/Analysis/Normed/Group/Basic.lean

feat: port Analysis.Normed.Group.Basic (#2736)

Added dist_one_left View on Github →