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 231b27e commit 51ac3abCopy full SHA for 51ac3ab
LeanCamCombi/ProbLYM.lean
@@ -49,7 +49,7 @@ theorem cardNumbering : card (Numbering α) = (card α).factorial := by
49
exact Fintype.card_equiv (Fintype.equivFinOfCardEq rfl)
50
51
omit [Fintype α] in
52
-theorem numbering_on_card (s : Finset α) : card (NumberingOn s) = s.card.factorial := by
+theorem card_numberingOn (s : Finset α) : card (NumberingOn s) = s.card.factorial := by
53
simp only [NumberingOn]
54
have h1 : card {x // x ∈ s} = card (Fin s.card) := by simp
55
have h2 : {x // x ∈ s} ≃ (Fin s.card) := by exact Fintype.equivOfCardEq h1
0 commit comments