The cardinality of Fin 2 is even.

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

Equations

• Fintype.IsSquare.decidablePred x✝ = Fintype.decidableExistsFintype

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

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