instFiniteDimensionalROfFinite — Mathlib

English

For finite σ, the kernel of evalᵢ σ K is the zero subspace: ker(evalᵢ σ K) = ⊥.

Русский

Для конечного σ ядерная область evalᵢ σ K тривиальна: ker(evalᵢ σ K) = ⊥.

LaTeX

$$$\\\\ker(\\\\mathrm{eval}_{i}\\\\sigma K) = \\\\{0\\\\}$$$

Lean4

instance [Finite σ] : FiniteDimensional K (R σ K) :=
  by
  cases nonempty_fintype σ
  classical
    exact
    IsNoetherian.iff_fg.1
      (IsNoetherian.iff_rank_lt_aleph0.mpr <| by
        simpa only [rank_R] using Cardinal.nat_lt_aleph0 (Fintype.card (σ → K)))

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