natCard_of_splits — Mathlib

English

If minpolynomials split in L for all x ∈ E, then the number of F-algebra homomorphisms E → F is equal to finrank F E.

Русский

Если все минполиномы для x ∈ E распадаются в L, то количество F-алгоморфизмов E→L равно конечной размерности E над F.

LaTeX

$$$\operatorname{Nat.card}(E\to_{F} L) = \operatorname{finrank} F E$$$

Lean4

theorem natCard_of_splits (L : Type*) [Field L] [Algebra F L] (hL : ∀ x : E, (minpoly F x).Splits (algebraMap F L)) :
    Nat.card (E →ₐ[F] L) = finrank F E :=
  (AlgHom.natCard_of_powerBasis (L := L) (Field.powerBasisOfFiniteOfSeparable F E)
          (Algebra.IsSeparable.isSeparable _ _) <|
        hL _).trans
    (PowerBasis.finrank _).symm

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