ι✝ : Type ?u.537278
ι' : Type ?u.537281
R : Type u_2
K : Type ?u.537287
A : Type u_3
A' : Type ?u.537293
A'' : Type ?u.537296
V : Type u
V' : Type ?u.537301
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
ι : Type u_1
f : ι → A
hf : AlgebraicIndependent R f
✝ : Nontrivial R
⊢ AlgebraicIndependent R Subtype.val
ι✝ : Type ?u.537278
ι' : Type ?u.537281
R : Type u_2
K : Type ?u.537287
A : Type u_3
A' : Type ?u.537293
A'' : Type ?u.537296
V : Type u
V' : Type ?u.537301
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
ι : Type u_1
f : ι → A
hf : AlgebraicIndependent R f
⊢ AlgebraicIndependent R Subtype.val
nontriviality R
no goals
ι✝ : Type ?u.537278
ι' : Type ?u.537281
R : Type u_2
K : Type ?u.537287
A : Type u_3
A' : Type ?u.537293
A'' : Type ?u.537296
V : Type u
V' : Type ?u.537301
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
ι : Type u_1
f : ι → A
hf : AlgebraicIndependent R f
✝ : Nontrivial R
⊢ AlgebraicIndependent R Subtype.val
rwa [algebraicIndependent_subtype_range hf.injective]