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 7820cf4 commit 231b27eCopy full SHA for 231b27e
LeanCamCombi/ProbLYM.lean
@@ -45,7 +45,7 @@ def NumberingOn {α : Type*} (s : Finset α) := {x // x ∈ s} ≃ Fin s.card
45
46
variable {α : Type*} [Fintype α] [DecidableEq α]
47
48
-theorem numbering_card : card (Numbering α) = (card α).factorial := by
+theorem cardNumbering : card (Numbering α) = (card α).factorial := by
49
exact Fintype.card_equiv (Fintype.equivFinOfCardEq rfl)
50
51
omit [Fintype α] in
0 commit comments