Def Mathlib.Tactic.Reassoc.registerReassocExpr

Modification history

2026-01-21 16:04
Mathlib/Tactic/CategoryTheory/Reassoc.lean
feat(reassoc): tag the generated declaration with `to_dual none` (#33833) …
Added Mathlib.Tactic.Reassoc.registerReassocExprView on Github →