.. _discrete_mathematics: Discrete Mathematics ==================== *Discrete Mathematics* is the study of finite sets, objects, and structures. We can count the elements of a finite set, and we can compute finite sums or products over its elements, we can compute maximums and minimums, and so on. We can also study objects that are generated by finitely many applications of certain generating functions, we can define functions by structural recursion, and prove theorems by structural induction. This chapters describes parts of Mathlib that support these activities. .. include:: C06_Discrete_Mathematics/S01_Finsets_and_Fintypes.inc .. include:: C06_Discrete_Mathematics/S02_Counting_Arguments.inc .. include:: C06_Discrete_Mathematics/S03_Inductive_Structures.inc