Def Mathlib.Tactic.Translate.translateLemmas

Modification history

2026-07-08 18:17
Mathlib/Tactic/Translate/Core.lean
feat(Translate): validate all translations (#40365) …
Modified Mathlib.Tactic.Translate.translateLemmasView on Github →
2026-05-11 22:46
Mathlib/Tactic/Translate/Core.lean
feat(to_additive): support `(attr := reassoc)` (#38994) …
Modified Mathlib.Tactic.Translate.translateLemmasView on Github →
2025-11-13 23:13
Mathlib/Tactic/ToAdditive/Frontend.lean
feat: `to_dual` attribute (#27887) …
Added Mathlib.Tactic.Translate.translateLemmasView on Github →