mathlib3 documentation

data.fintype.parity

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
@[protected, instance]
def fintype.is_square.decidable_pred {α : Type u_1} [has_mul α] [fintype α] [decidable_eq α] :
decidable_pred is_square
Equations
source
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.special_linear_group.has_neg.