fintype — Mathlib

English

If E/F is finite-dimensional, then the set of F-algebra homomorphisms E →ₐ[F] K is finite; i.e., Fintype(E →ₐ[F] K).

Русский

Если расширение E/F конечно размерно, то множество F-алгоморфизмов E →ₐ[F] K конечно; то есть существует конечное множество таких гомоморфизмов.

LaTeX

$$$\text{Fintype }(E \to_A[F] K)$$$

Lean4

/-- Given field extensions `E/F` and `K/F`, with `E/F` finite, there are finitely many `F`-algebra
  homomorphisms `E →ₐ[K] K`. -/
noncomputable instance fintype : Fintype (E →ₐ[F] K) :=
  @Fintype.ofInjective _ _ (Fintype.subtypeProd (finite_range (Module.finBasis F E)) fun e => (minpoly F e).aroots K) _
    (aux_inj_roots_of_min_poly F E K)

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