Shrink

📁 Source: Mathlib/Data/Fintype/Shrink.lean

Statistics

Metric	Count
Definitions instFintype	1
Theorems card_shrink, instFinite	2
Total	3

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_shrink 📖	mathematical	—	card Shrink Countable.toSmall Finite.to_countable Finite.of_fintype	—	Countable.toSmall Finite.to_countable Finite.of_fintype card_congr

Shrink

Definitions

Name	Category	Theorems
instFintype 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFinite 📖	mathematical	—	Finite Shrink Countable.toSmall Finite.to_countable	—	Finite.of_equiv Countable.toSmall Finite.to_countable

---

← Back to Index