Commit 2026-09-22 06:19 7d680cae
View on Github →chore: fix instance and to_additive declaration names (#44052)
Fixes the names of three misspelled instances and two @[to_additive] theorems. Both halves need the alias itself reviewed rather than the name, which is why they are together and separate from the plain spelling fixes.
Split out of #43889.
Written with the assistance of Claude (Claude Code).