Commit 2026-06-15 00:50 439c664b

View on Github →

chore(Counterexamples/DirectSumIsInternal): fix defLemma error (#40592) As could be seen from running #lint in that file. The new defProp linter in Lean core also flagged this.

Estimated changes