Def ToAdditive.abbreviationDict

Modification history

2025-11-13 23:13
Mathlib/Tactic/ToAdditive/GuessName.lean
feat: `to_dual` attribute (#27887) …
Deleted ToAdditive.abbreviationDictView on Github →
2025-11-12 23:50
Mathlib/Tactic/ToAdditive/GuessName.lean
refactor: simplify dictionary in fixAbbreviation (#29352) …
Added ToAdditive.abbreviationDictView on Github →