Finite

📁 Source: Mathlib/Combinatorics/Derangements/Finite.lean

Statistics

Metric	Count
Definitions instDecidablePredPermDerangements, instFintypeElemPermDerangements, numDerangements	3
Theorems card_derangements_eq_numDerangements, card_derangements_fin_add_two, card_derangements_fin_eq_numDerangements, card_derangements_invariant, numDerangements_add_two, numDerangements_one, numDerangements_succ, numDerangements_sum, numDerangements_zero	9
Total	12

(root)

Definitions

Name	Category	Theorems
instDecidablePredPermDerangements 📖	CompOp	—
instFintypeElemPermDerangements 📖	CompOp	4 math math: card_derangements_invariant, card_derangements_fin_add_two, card_derangements_eq_numDerangements, card_derangements_fin_eq_numDerangements
numDerangements 📖	CompOp	8 math math: numDerangements_succ, numDerangements_add_two, numDerangements_one, numDerangements_sum, numDerangements_tendsto_inv_e, card_derangements_eq_numDerangements, card_derangements_fin_eq_numDerangements, numDerangements_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_derangements_eq_numDerangements 📖	mathematical	—	Fintype.card Set.Elem Equiv.Perm derangements instFintypeElemPermDerangements numDerangements	—	card_derangements_invariant Fintype.card_fin card_derangements_fin_eq_numDerangements
card_derangements_fin_add_two 📖	mathematical	—	Fintype.card Set.Elem Equiv.Perm derangements instFintypeElemPermDerangements Fin.fintype	—	Fintype.card_ofFinset Finset.filter.congr_simp Finset.filter_ne' Finset.card_erase_of_mem Finset.mem_univ Finset.card_fin add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Fintype.card_fin Fintype.card_option card_derangements_invariant Fintype.card_congr Fintype.card_sigma Finset.sum_congr Fintype.card_sum Finset.sum_const nsmul_eq_mul mul_add Distrib.leftDistribClass
card_derangements_fin_eq_numDerangements 📖	mathematical	—	Fintype.card Set.Elem Equiv.Perm derangements instFintypeElemPermDerangements Fin.fintype numDerangements	—	numDerangements_add_two card_derangements_fin_add_two mul_add Distrib.leftDistribClass
card_derangements_invariant 📖	mathematical	Fintype.card	Set.Elem Equiv.Perm derangements instFintypeElemPermDerangements	—	Fintype.card_congr
numDerangements_add_two 📖	mathematical	—	numDerangements	—	—
numDerangements_one 📖	mathematical	—	numDerangements	—	—
numDerangements_succ 📖	mathematical	—	numDerangements Monoid.toNatPow Int.instMonoid	—	pow_succ Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
numDerangements_sum 📖	mathematical	—	numDerangements Finset.sum Int.instAddCommMonoid Finset.range Monoid.toNatPow Int.instMonoid Nat.ascFactorial	—	Finset.sum_range_succ numDerangements_succ Finset.mul_sum tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub Nat.ascFactorial_zero mul_one pow_succ' neg_one_mul sub_eq_add_neg AddRightCancelSemigroup.toIsRightCancelAdd Finset.sum_congr Finset.mem_range_succ_iff Nat.ascFactorial_succ add_right_comm add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid mul_left_comm Nat.cast_one
numDerangements_zero 📖	mathematical	—	numDerangements	—	—

---

← Back to Index