Theorems · Theorem · commutative algebra

transcendental_aeval_iff

∀ {K : Type u_1} {A : Type u_4} [inst : Field K] [inst_1 : Ring A] [inst_2 : Algebra K A] {r : A} {f : Polynomial K},
  Transcendental K ((Polynomial.aeval r) f) ↔ Transcendental K r ∧ Transcendental K f

If K is a field, r : A and f : K[X], then Polynomial.aeval r f is transcendental over K if and only if r and f are both transcendental over K. See also Transcendental.aeval_of_transcendental and Transcendental.of_aeval.

Defined in

Mathlib.RingTheory.Algebraic.Integral

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldRingAlgebra