cardinalMk_algHom — Mathlib

English

There is a bound on the number of algebra homomorphisms from V to W in terms of finrank(W, V→_L V).

Русский

Число алгебраических гомоморфизмов ограничено по финрэнку пространства линейных отображений.

LaTeX

$$$|V \\to_K W| \\le \\operatorname{finrank}_K(W, V \\to_L[K] W)$$$

Lean4

theorem cardinalMk_algHom (K : Type u) (V : Type v) (W : Type w) [Field K] [Ring V] [Algebra K V]
    [FiniteDimensional K V] [Field W] [Algebra K W] : Cardinal.mk (V →ₐ[K] W) ≤ finrank W (V →ₗ[K] W) :=
  (linearIndependent_toLinearMap K V W).cardinalMk_le_finrank

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