Commit 2023-06-17 07:00 caba0f01

View on Github →

chore: have CI run on tests in subdirectories (#5065) Also fix bug in elementwise that wasn't caught while tests weren't running.

Estimated changes

Modified GNUmakefile

Modified Mathlib/Tactic/CategoryTheory/Elementwise.lean

modified theorem Tactic.Elementwise.forget_hom_Type

Modified test/CategoryTheory/Elementwise.lean