Cardinality_of_Cartesian_Product
Provedcardinalitycardinality-of-cartesian-productcartesian-productcombinatoricsproofwiki
Let be the cartesian product of two finite sets and . Then where denotes cardinality.
Preamble
import Mathlib.Data.Fintype.Prod
Formal statement
theorem Cardinality_of_Cartesian_Product {S T : Type _} [Fintype S] [Fintype T] : Fintype.card (S × T) = Fintype.card S * Fintype.card T := by sorrySource