English
If k is a finite field and V has finite k-dimension n, then the cardinality of the projective space ℙ_k V equals the sum ∑_{i=0}^{n-1} (|k|)^i.
Русский
Если k — конечное поле, а размерность V над k равна n, то кардинальность пространства проективного ℙ_k V равна сумме ∑_{i=0}^{n-1} (|k|)^i.
LaTeX
$$$|\\mathbb{P}_k V| = \\sum_{i=0}^{n-1} |k|^i \\quad\\text{where } n = \\operatorname{finrank}_k V$$$
Lean4
theorem card_of_finrank [Finite k] {n : ℕ} (h : Module.finrank k V = n) :
Nat.card (ℙ k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i :=
by
wlog hf : Finite V
· have : Infinite (ℙ k V) := by
contrapose! hf
rwa [finite_iff_of_finite] at hf
have : n = 0 := by
rw [← h]
apply Module.finrank_of_not_finite
contrapose! hf
simpa using Module.finite_of_finite k
simp [this]
have : 1 < Nat.card k := Finite.one_lt_card
refine Nat.mul_right_cancel (m := Nat.card k - 1) (by cutsat) ?_
let e : V ≃ₗ[k] (Fin n → k) := LinearEquiv.ofFinrankEq _ _ (by simpa)
have hc : Nat.card V = Nat.card k ^ n := by simp [Nat.card_congr e.toEquiv, Nat.card_fun]
zify
conv_rhs => rw [Int.natCast_sub this.le, Int.natCast_one, geom_sum_mul]
rw [← Int.natCast_mul, ← card k V, hc]
simp
