card'' — Mathlib

English

Let k be a finite field and V a finite-dimensional vector space over k. Then the number of points of the projective space ℙ_k V is given by the formula |ℙ_k V| = (|V| − 1)/(|k| − 1).

Русский

Пусть k — конечное поле, а V — конечноразмерное векторное пространство над k. Тогда число точек проективного пространства ℙ_k V удовлетворяет формуле |ℙ_k V| = (|V| − 1)/(|k| − 1).

LaTeX

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

Lean4

/-- Cardinality formula for the points of `ℙ k V` if `k` and `V` are finite expressed
as a fraction. -/
theorem card'' [Finite k] : Nat.card (ℙ k V) = (Nat.card V - 1) / (Nat.card k - 1) :=
  by
  have : 1 < Nat.card k := Finite.one_lt_card
  rw [card k, Nat.mul_div_cancel]
  cutsat

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