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.