Theorem CategoryTheory.eq_whisker'

Modification history

2026-01-21 16:04

Mathlib/Tactic/CategoryTheory/Reassoc.lean

feat(reassoc): tag the generated declaration with `to_dual none` (#33833) …

Deleted CategoryTheory.eq_whisker'View on Github →

2025-12-13 14:21

Mathlib/Tactic/CategoryTheory/Reassoc.lean

chore: use `Category*` everywhere (#32842) …

Modified CategoryTheory.eq_whisker'View on Github →

2025-08-28 22:46

Mathlib/Tactic/CategoryTheory/Reassoc.lean

feat: make `reassoc_of%` be able to defer `Category` instance (#26130) …

Modified CategoryTheory.eq_whisker'View on Github →

2022-12-01 15:35

Mathlib/Tactic/Reassoc.lean

port: several files from category_theory (#749) …

Added CategoryTheory.eq_whisker'View on Github →