We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 53a2db6 commit ca537f2Copy full SHA for ca537f2
1 file changed
Mathlib/Combinatorics/SimpleGraph/Copy.lean
@@ -526,7 +526,7 @@ lemma copyCount_eq_card_image_copyToSubgraph [Fintype (H.Copy G)]
526
Nat.card_eq_fintype_card, Fintype.card_coe]
527
528
@[simp] lemma copyCount_eq_zero [Finite V] : G.copyCount H = 0 ↔ H.Free G := by
529
- rw [copyCount, Nat.card_eq_zero]
+ rw [copyCount, Nat.card_eq_zero]
530
constructor <;> intro h
531
· obtain h1 | h2 := h
532
· rw [Free, isContained_iff_exists_iso_subgraph]
0 commit comments