Commit 2026-08-14 12:19 0d80b877
View on Github →chore(SimpleGraph/Clique): tidy CliqueFree iff lemmas (#41364)
Add G.CliqueFree n ↔ (completeGraph (Fin n)).Free G and rename two other iff theorems to fit better.
Since Free is not infix it should come before top when naming, cliqueFree_iff should mention its RHS since it isn't obvious, and Fintype.card should be mentioned.