Commit 2025-02-03 06:56 cd5fbfb7
View on Github →chore: replace the lemma that dist 1 = norm
by dist 1 a = ‖a‖
(#21340)
This is much easier to use in rw
as one can specify which occurrence to target.
chore: replace the lemma that dist 1 = norm
by dist 1 a = ‖a‖
(#21340)
This is much easier to use in rw
as one can specify which occurrence to target.