The cardinality of Fin (bit0 n)
is even. #
instance
Fintype.IsSquare.decidablePred
{α : Type u_1}
[inst : Mul α]
[inst : Fintype α]
[inst : DecidableEq α]
:
DecidablePred IsSquare
Equations
- Fintype.IsSquare.decidablePred x = Fintype.decidableExistsFintype
The cardinality of Fin (bit0 n)
is even, fact
version.
This fact
is needed as an instance by Matrix.SpecialLinearGroup.has_neg
.