Theorems · Theorem · field theory

IsTranscendenceBasis.of_comp

∀ {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : CommRing A'] [inst_3 : Algebra R A] [inst_4 : Algebra R A'] {x : ι → A} (f : A →ₐ[R] A'),
  Function.Injective ⇑f → IsTranscendenceBasis R (⇑f ∘ x) → IsTranscendenceBasis R x

Defined in

Mathlib.RingTheory.AlgebraicIndependent.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRingAlgebraAlgebra