mathlib documentation

data.fintype.parity

The cardinality of fin (bit0 n) is even. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem fintype.card_fin_even {n : } :

The cardinality of fin (bit0 n) is even, fact version. This fact is needed as an instance by matrix.special_linear_group.has_neg.