finite_of_finite — Mathlib

English

If k is finite and V is finite, then ℙ_k(V) is finite.

Русский

Если k конечно и V конечномерно, то ℙ_k(V) конечно.

LaTeX

$$[Finite k] [Finite V] ⇒ Finite (ℙ_k(V))$$

Lean4

/-- If `V` is a finite `k`-module and `k` is finite, `ℙ k V` is finite. -/
instance finite_of_finite [Finite V] : Finite (ℙ k V) :=
  have : Finite (ℙ k V × kˣ) := Finite.of_equiv _ (nonZeroEquivProjectivizationProdUnits k V)
  Finite.prod_left kˣ

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