Theorems · Definition · commutative algebra

PowerBasis.AlgHom.fintype

{S : Type u_2} →
  [inst : Ring S] →
    {A : Type u_4} →
      {B : Type u_5} →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing B] →
            [inst_3 : Algebra A B] → [inst_4 : Algebra A S] → [IsDomain B] → PowerBasis A S → Fintype (S →ₐ[A] B)

There are finitely many algebra homomorphisms S →ₐ[A] B if S is of the form A[x] and B is an integral domain.

Defined in

Mathlib.RingTheory.PowerBasis

Cited by

5 results in Mathlib

Foundations

Depth 138 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingCommRingCommRingAlgebraAlgebraIsDomain