Def Test.mulMatchAux

Modification history

2025-12-04 17:49

MathlibTest/toAdditive.lean

fix(to_additive): use `findRelevantArg` for auxiliarly declarations (#32404) …

Added Test.mulMatchAux View on Github →