ι : Type u_4
ι' : Type ?u.331344
R : Type u_1
K : Type ?u.331350
A : Type u_2
A' : Type u_3
A'' : Type ?u.331359
V : Type u
V' : Type ?u.331364
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (↑f ∘ x)
this : aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
⊢ AlgebraicIndependent R x
ι : Type u_4
ι' : Type ?u.331344
R : Type u_1
K : Type ?u.331350
A : Type u_2
A' : Type u_3
A'' : Type ?u.331359
V : Type u
V' : Type ?u.331364
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (↑f ∘ x)
⊢ AlgebraicIndependent R x
have : aeval (f ∘ x) = f.comp (aeval x) := by ext; simp
ι : Type u_4
ι' : Type ?u.331344
R : Type u_1
K : Type ?u.331350
A : Type u_2
A' : Type u_3
A'' : Type ?u.331359
V : Type u
V' : Type ?u.331364
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hfv : Injective (↑f ∘ ↑(aeval x))
this : aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
⊢ AlgebraicIndependent R x
ι : Type u_4
ι' : Type ?u.331344
R : Type u_1
K : Type ?u.331350
A : Type u_2
A' : Type u_3
A'' : Type ?u.331359
V : Type u
V' : Type ?u.331364
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (↑f ∘ x)
this : aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
⊢ AlgebraicIndependent R x
rw [AlgebraicIndependent, this, AlgHom.coe_comp] at hfv
no goals
ι : Type u_4
ι' : Type ?u.331344
R : Type u_1
K : Type ?u.331350
A : Type u_2
A' : Type u_3
A'' : Type ?u.331359
V : Type u
V' : Type ?u.331364
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hfv : Injective (↑f ∘ ↑(aeval x))
this : aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
⊢ AlgebraicIndependent R x
exact hfv.of_comp
case hf
ι : Type u_4
ι' : Type ?u.331344
R : Type u_1
K : Type ?u.331350
A : Type u_2
A' : Type u_3
A'' : Type ?u.331359
V : Type u
V' : Type ?u.331364
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (↑f ∘ x)
i✝ : ι
⊢ ↑(aeval (↑f ∘ x)) (X i✝) = ↑(AlgHom.comp f (aeval x)) (X i✝)
ι : Type u_4
ι' : Type ?u.331344
R : Type u_1
K : Type ?u.331350
A : Type u_2
A' : Type u_3
A'' : Type ?u.331359
V : Type u
V' : Type ?u.331364
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (↑f ∘ x)
⊢ aeval (↑f ∘ x) = AlgHom.comp f (aeval x)
ext
no goals
case hf
ι : Type u_4
ι' : Type ?u.331344
R : Type u_1
K : Type ?u.331350
A : Type u_2
A' : Type u_3
A'' : Type ?u.331359
V : Type u
V' : Type ?u.331364
x : ι → A
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing A'
inst✝³ : CommRing A''
inst✝² : Algebra R A
inst✝¹ : Algebra R A'
inst✝ : Algebra R A''
a b : R
hx : AlgebraicIndependent R x
f : A →ₐ[R] A'
hfv : AlgebraicIndependent R (↑f ∘ x)
i✝ : ι
⊢ ↑(aeval (↑f ∘ x)) (X i✝) = ↑(AlgHom.comp f (aeval x)) (X i✝)
simp