ToAdditive
📁 Source: Mathlib/Tactic/Translate/ToAdditive.lean
Statistics
| Metric | Count |
|---|---|
| 12 | |
| Theorems | 0 |
| Total | 12 |
Mathlib.Tactic.ToAdditive
Definitions
| Name | Category | Theorems |
|---|---|---|
abbreviationDict 📖 | CompOp | — |
attrTo_additive?_ 📖 | CompOp | — |
commandInsert_to_additive_translation__ 📖 | CompOp | — |
data 📖 | CompOp | — |
doTranslateAttr 📖 | CompOp | — |
ignoreArgsAttr 📖 | CompOp | — |
nameDict 📖 | CompOp | — |
to_additive 📖 | CompOp | — |
to_additive_do_translate 📖 | CompOp | — |
to_additive_dont_translate 📖 | CompOp | — |
to_additive_ignore_args 📖 | CompOp | — |
translations 📖 | CompOp | — |
---