The cardinality of Fin 2 is even.

@[implicit_reducible]

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

instance Fintype.card_fin_two : Fact (Even (card (Fin 2)))

The cardinality of Fin 2 is even, Fact version. This Fact is needed as an instance by Matrix.SpecialLinearGroup.instNeg.