card_of_splits — Mathlib

English

For L with the split condition for all x, the cardinal of AlgHom F E L equals finrank F E.

Русский

Для L со свойством распада минполиномов будет кардинал гомоморфизмов E→L равен размерности E над F.

LaTeX

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

Lean4

@[simp]
theorem card_of_splits (L : Type*) [Field L] [Algebra F L] (hL : ∀ x : E, (minpoly F x).Splits (algebraMap F L)) :
    Fintype.card (E →ₐ[F] L) = finrank F E := by rw [Fintype.card_eq_nat_card, AlgHom.natCard_of_splits F E L hL]

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