Mathlib v3 is deprecated. Go to Mathlib v4

Theorem prod.card_Icc

Modification history

2022-10-16 18:10
src/order/locally_finite.lean
feat(order/locally_finite): add lemmas expanding `finset.Icc` (#16996) …
Added prod.card_IccView on Github →