card_fin_two

Mathlib.Data.Fintype.Parity

URI: https://scilib.ai/kg/mathlib#Fintype.card_fin_two

← MathLib Explorer

English

The cardinality of Fin 2 is even.

Русский

Кардинал_FIN_2 или кардинал Fin 2 чётен.

LaTeX

$$$Even\\bigl(Fintype.card\\,(Fin\\ 2)\\bigr).$$$

Lean4

/-- The cardinality of `Fin 2` is even, `Fact` version.
This `Fact` is needed as an instance by `Matrix.SpecialLinearGroup.instNeg`. -/
instance card_fin_two : Fact (Even (Fintype.card (Fin 2))) :=
  ⟨⟨1, rfl⟩⟩

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru