fintypeOfAlgHomAdjoinIntegral — Mathlib

English

There is a finite type structure on the set of F-algebra homomorphisms F⟮α⟯ →ₐ[F] K, given by the power basis.

Русский

Существуют конечномерные отображения алгеброморфизмов F⟮α⟯ →ₐ[F] K, задаваемые через базис мощности.

LaTeX

$$Fintype (F⟮α⟯ →ₐ[F] K)$$

Lean4

/-- Fintype of algebra homomorphism `F⟮α⟯ →ₐ[F] K` -/
noncomputable def fintypeOfAlgHomAdjoinIntegral (h : IsIntegral F α) : Fintype (F⟮α⟯ →ₐ[F] K) :=
  PowerBasis.AlgHom.fintype (adjoin.powerBasis h)

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