Commit 2024-02-29 17:22 64848f61
View on Github →add two to_additive name translations (#10831)
- Remove manual translations that are now guessed correctly
- Fix some names that were incorrectly guessed by humans (and in one case fix the multiplicative name). Add deprecations for all name changes.
- Remove a couple manually additivized lemmas.