card_of_powerBasis — Mathlib

English

Under the same hypotheses as above, the finite cardinality of AlgHom K S L equals pb.dim.

Русский

При тех же предположениях число гомоморфизмов по K от S в L равно pb.dim.

LaTeX

$$$|S \\to_K L| = pb.dim$$$

Lean4

theorem card_of_powerBasis (pb : PowerBasis K S) (h_sep : IsSeparable K pb.gen)
    (h_splits : (minpoly K pb.gen).Splits (algebraMap K L)) :
    @Fintype.card (S →ₐ[K] L) (PowerBasis.AlgHom.fintype pb) = pb.dim := by
  classical rw [Fintype.card_eq_nat_card, AlgHom.natCard_of_powerBasis pb h_sep h_splits]

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