Theorems · Definition · field theory

Polynomial.algEquivOfTranscendental

(R : Type u_1) →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : Ring S] → [inst_2 : Algebra R S] → (s : S) → Transcendental R s → Polynomial R ≃ₐ[R] ↥R[s]

Given a transcendental element s : S over R, the R-algebra equivalence between R[X] and R[s] given by sending X to s.

Defined in

Mathlib.RingTheory.Algebraic.Basic

Cited by

11 results in Mathlib

Foundations

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

Assumes

CommRingRingAlgebra