Commit 2025-09-27 11:48 cfc33f40
View on Github →chore(Order): untangle imports by moving IsAntichain lemmas (#29993)
Right now Minimal.lean imports Antichain.lean to prove some lemmas about antichains. This is an unnecessary import, since those lemmas can live in Antichain.lean with no additional imports, and thereby reduce the imports in Minimal.lean (and this helps prevent circular includes for another PR of mine.)