Def Mathlib.Tactic.Translate.addTranslationFor

Modification history

2026-10-04 05:36

Mathlib/Tactic/Translate/Core.lean

feat(Translate): implementation of `to_dual_for` command (#44270) …

Added Mathlib.Tactic.Translate.addTranslationFor View on Github →