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.

Estimated changes