English
If V is finite then |V| − 1 = |ℙ_k(V)| · (|k| − 1).
Русский
Если V конечно, то |V| − 1 = |ℙ_k(V)| · (|k| − 1).
LaTeX
$$$ |V| - 1 = |\mathbb{P}_k(V)| \cdot (|k| - 1) $$$
Lean4
/-- Fraction free cardinality formula for the points of `ℙ k V` if `k` and `V` are finite
(for silly reasons the formula also holds when `k` and `V` are infinite).
See `Projectivization.card'` and `Projectivization.card''` for other spellings of the formula. -/
theorem card : Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1) :=
by
nontriviality V
cases finite_or_infinite k with
| inr h =>
have : Infinite V := Module.Free.infinite k V
simp
| inl h =>
cases finite_or_infinite V with
| inr h =>
have := not_iff_not.mpr (finite_iff_of_finite k V)
push_neg at this
have : Infinite (ℙ k V) := by rwa [this]
simp
| inl h =>
classical
haveI : Fintype V := Fintype.ofFinite V
haveI : Fintype (ℙ k V) := Fintype.ofFinite (ℙ k V)
haveI : Fintype k := Fintype.ofFinite k
have hV : Fintype.card { v : V // v ≠ 0 } = Fintype.card V - 1 := by simp
simp_rw [← Fintype.card_eq_nat_card, ← Fintype.card_units (α := k), ← hV]
rw [Fintype.card_congr (nonZeroEquivProjectivizationProdUnits k V), Fintype.card_prod]
