Commit 2025-11-04 11:38 282887a1

View on Github →

chore(Tactic/CategoryTheory/Coherence): fix copyright headers (#31252) Both files were originally one file, the Lean 4 port of the coherence tactic. That one was initially written by Kim Morrison in mathlib#13125. It appears that omitting the copyright holder was a mere oversight.

Estimated changes