finite_iff_of_finite — Mathlib

English

ℙ_k(V) is finite if and only if V is finite when k is finite.

Русский

ℙ_k(V) конечно тогда и только тогда, когда V конечномерно, при конечном поле k.

LaTeX

$$$ Finite k \Rightarrow (Finite (\mathbb{P}_k(V)) \Leftrightarrow Finite V)$$$

Lean4

theorem finite_iff_of_finite [Finite k] : Finite (ℙ k V) ↔ Finite V := by
  classical
  refine ⟨fun h ↦ ?_, fun h ↦ inferInstance⟩
  let e := nonZeroEquivProjectivizationProdUnits k V
  have : Finite { v : V // v ≠ 0 } := Finite.of_equiv _ e.symm
  let eq : { v : V // v ≠ 0 } ⊕ Unit ≃ V :=
    ⟨(Sum.elim Subtype.val (fun _ ↦ 0)), fun v ↦ if h : v = 0 then Sum.inr () else Sum.inl ⟨v, h⟩, by intro x; aesop, by
      intro x; aesop⟩
  exact Finite.of_equiv _ eq

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