Theorems · Theorem · field theory

Transcendental.of_aeval

∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : A} {f : Polynomial R},
  Transcendental R ((Polynomial.aeval r) f) → Transcendental R f

If Polynomial.aeval r f is transcendental over R, then f : R[X] is also transcendental over R. In fact, the r is also transcendental over R provided that R is a field (see transcendental_aeval_iff).

Defined in

Mathlib.RingTheory.Algebraic.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingRingAlgebra