The cardinality of Fin (bit0 n) is even.

ink

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

Equations

• Fintype.IsSquare.decidablePred x = Fintype.decidableExistsFintype

ink

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.