Commit 2026-05-09 23:47 26c4381a

feat(Translate): locally modify name guessing dictionaries (#37808) This PR adds the feature to to_dual and to_additive that you can now locally modify the name translation dictionary. With this change, we run the risk of having the automated translations being harder to predict. For this reason, the changes to the dictionary do not persisted through imports. Instead, the change lasts until the end of the file (though it ignores sections). See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Order.20dual.20tactic/near/580834166