card_of_finrank_two — Mathlib

English

If the dimension n of V over a finite field k is 2, then the cardinality of the projective space ℙ_k V is |k| + 1.

Русский

Если размерность V над конечным полем k равна 2, то кардинальность проективного пространства ℙ_k V равна |k| + 1.

LaTeX

$$$|\mathbb{P}_k V| = |k| + 1$$$

Lean4

theorem card_of_finrank_two [Finite k] (h : Module.finrank k V = 2) : Nat.card (ℙ k V) = Nat.card k + 1 := by
  simp [card_of_finrank k V h]

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