The cardinality of Fin (bit0 n) is even.

instance Fintype.IsSquare.decidablePred {α : Type u_1} [Mul α] [Fintype α] [DecidableEq α] : DecidablePred IsSquare

theorem Fintype.card_fin_even {n : ℕ} : Fact (Even (Fintype.card (Fin (bit0 n))))

The cardinality of Fin (bit0 n) is even, Fact version. This Fact is needed as an instance by Matrix.SpecialLinearGroup.has_neg.