Def Mathlib.Tactic.Reassoc.reassocExpr'

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.reassocExpr'View on Github →