ι : Type u_2
ι' : Type u_1
R : Type u_3
K : Type ?u.166980
A : Type u_4
A' : Type ?u.166986
A'' : Type ?u.166989
V : Type u
V' : Type ?u.166994
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 : ι' → ι
hf : Injective f
p q : MvPolynomial ι' R
⊢ ↑(aeval (x ∘ f)) p = ↑(aeval (x ∘ f)) q → p = q
ι : Type u_2
ι' : Type u_1
R : Type u_3
K : Type ?u.166980
A : Type u_4
A' : Type ?u.166986
A'' : Type ?u.166989
V : Type u
V' : Type ?u.166994
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 : ι' → ι
hf : Injective f
⊢ AlgebraicIndependent R (x ∘ f)
intro p q
no goals
ι : Type u_2
ι' : Type u_1
R : Type u_3
K : Type ?u.166980
A : Type u_4
A' : Type ?u.166986
A'' : Type ?u.166989
V : Type u
V' : Type ?u.166994
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 : ι' → ι
hf : Injective f
p q : MvPolynomial ι' R
⊢ ↑(aeval (x ∘ f)) p = ↑(aeval (x ∘ f)) q → p = q
simpa [aeval_rename, (rename_injective f hf).eq_iff] using @hx (rename f p) (rename f q)