card_algHom_le_finrank — Mathlib

English

The number of K-algebra homomorphisms from M to L is at most finrank(K,M).

Русский

Количество K-алгоморфизмов из M в L не превосходит finrank(K,M).

LaTeX

$$$$ \#(\mathrm{AlgHom}_K(M, L)) \le \mathrm{finrank}_K M. $$$$

Lean4

@[stacks 09HS]
theorem card_algHom_le_finrank : Nat.card (M →ₐ[K] L) ≤ finrank K M :=
  by
  convert toNat_le_toNat (cardinalMk_algHom_le_rank K M L) ?_
  · rw [toNat_lift, finrank]
  · rw [lift_lt_aleph0]; have := Module.nontrivial K L; apply Module.rank_lt_aleph0

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