Def ToAdditive.findTargetName

Modification history

2023-02-04 00:58

Mathlib/Tactic/ToAdditive.lean

fix: interaction between to_additive and rewriting definitions (#1948)

Added ToAdditive.findTargetName View on Github →