Documentation

Mathlib.Data.Fintype.Parity

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

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

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