finiteDimensional_pi' — Mathlib

English

If ι is finite, then (ι → K) is finite-dimensional over K for a field K.

Русский

Если индекс ι конечен, то пространство функционалов ι → K конечномерно над K.

LaTeX

$$Finite ι ⇒ FiniteDimensional(K, ι → K)$$

Lean4

instance finiteDimensional_pi' {ι : Type*} [Finite ι] (M : ι → Type*) [∀ i, AddCommGroup (M i)] [∀ i, Module K (M i)]
    [∀ i, FiniteDimensional K (M i)] : FiniteDimensional K (∀ i, M i) :=
  Finite.pi

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