Skip to content

Commit fe1931e

Browse files
Remove placeholder
1 parent ff25836 commit fe1931e

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

  • Mathlib/Combinatorics/SimpleGraph/Extremal

Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -399,7 +399,7 @@ theorem CliqueFree.card_edgeFinset_le (cf : G.CliqueFree (r + 1)) :
399399
simp_rw [zero_tsub, mul_zero, Nat.mod_zero, Nat.div_zero, zero_add]
400400
exact card_edgeFinset_le_card_choose_two
401401
· obtain ⟨H, _, maxH⟩ := exists_isTuranMaximal (V := V) hr
402-
convert maxH.2 _ cf
402+
convert maxH.2 cf
403403
rw [((isTuranMaximal_iff_nonempty_iso_turanGraph hr).mp maxH).some.card_edgeFinset_eq,
404404
card_edgeFinset_turanGraph]
405405

0 commit comments

Comments
 (0)