card_le — Mathlib

English

The number of F-automorphisms of K is at most finrank F K; i.e., Fintype.card (AlgHom F K K) ≤ Module.finrank F K.

Русский

Число автоморфизмов по F не превосходит размерности K над F.

LaTeX

$$$| \\operatorname{AlgHom}_F(K,K) | \\le \\operatorname{finrank}_F K$$$

Lean4

theorem card_le {F K : Type*} [Field F] [Field K] [Algebra F K] [FiniteDimensional F K] :
    Fintype.card (K ≃ₐ[F] K) ≤ Module.finrank F K :=
  Fintype.ofEquiv_card (algEquivEquivAlgHom F K).toEquiv.symm ▸ AlgHom.card_le

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