Theorems · Theorem · field theory

AlgebraicIndependent.of_ringHom_of_comp_eq

∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  {S : Type u_3} {B : Type u_4} {FRS : Type u_5} {FAB : Type u_6} [inst_3 : CommRing S] [inst_4 : CommRing B]
  [inst_5 : Algebra S B] [inst_6 : FunLike FRS R S] [inst_7 : RingHomClass FRS R S] [inst_8 : FunLike FAB A B]
  [inst_9 : RingHomClass FAB A B] (f : FRS) (g : FAB),
  AlgebraicIndependent S (⇑g ∘ x) →
    Function.Injective ⇑f → (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A) → AlgebraicIndependent R x

Defined in

Mathlib.RingTheory.AlgebraicIndependent.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingCommRingAlgebraFunLikeRingHomClassFunLikeRingHomClass