instMembershipProjectivizationForallFinOfNatNat

Mathlib.Combinatorics.Configuration

URI: https://scilib.ai/kg/mathlib#Configuration.ofField.instMembershipProjectivizationForallFinOfNatNat

English

Equivalently, the cardinality of P is n^2 + n + 1 where n is the plane order.

Русский

Эквивалентно: кардинальность P равна n^2 + n + 1, если порядок плоскости равен n.

LaTeX

$$$ Fintype.card P = (\operatorname{order} P L)^2 + (\operatorname{order} P L) + 1 $$$

Lean4

instance : Membership (ℙ K (Fin 3 → K)) (ℙ K (Fin 3 → K)) :=
  ⟨Function.swap orthogonal⟩

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

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

Разделы

Аффилиация

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