Documentation

Mathlib.Data.Fintype.Parity

The cardinality of Fin 2 is even. #

source
🔸 coverage
instance Fintype.IsSquare.decidablePred {α : Type u_1} [Mul α] [Fintype α] [DecidableEq α] :
DecidablePred IsSquare
Equations
    source
    📐 coverage
    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.