mathlib
3c1f3329 - feat(tactic/to_additive): automate substructure naming (#3553)

Commit
5 years ago
feat(tactic/to_additive): automate substructure naming (#3553) This is all @cipher1024's work, improving `to_additive` to correctly generate names when we're talking about structures (rather than just operations). Co-authored-by: Simon Hudon <simon.hudon@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading