Theorem: IndexType.card_prod (SciLean/Data/IndexType.lean)

State before:
ι✝ : Type v
inst✝² : IndexType ι✝
ι : Type u_1
κ : Type u_2
inst✝¹ : IndexType ι
inst✝ : IndexType κ
⊢ card (ι × κ) = card ι * card κ
Tactic:
rfl
State after:
no goals