Def ToAdditive.addCommPrefix

Modification history

2022-11-17 14:37

Mathlib/Tactic/ToAdditive.lean

feat: improve `ToAdditive.guessName` to work with capitalisation (#579) …

Deleted ToAdditive.addCommPrefix View on Github →

2022-05-11 23:41

Mathlib/Tactic/ToAdditive.lean

feat: `to_additive` (#234) …

Added ToAdditive.addCommPrefix View on Github →