ι✝ : Type ?u.747618
ι'✝ : Type ?u.747621
R : Type u_3
K : Type ?u.747627
A : Type u_4
A' : Type ?u.747633
A'' : Type ?u.747636
V : Type u
V' : Type ?u.747641
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
ι' : Type u_2
s : Set ι
f : ι → ι'
g : ι' → A
hs : AlgebraicIndependent R fun x => g (f ↑x)
✝ : Nontrivial R
⊢ AlgebraicIndependent R fun x => g ↑x
ι✝ : Type ?u.747618
ι'✝ : Type ?u.747621
R : Type u_3
K : Type ?u.747627
A : Type u_4
A' : Type ?u.747633
A'' : Type ?u.747636
V : Type u
V' : Type ?u.747641
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
ι' : Type u_2
s : Set ι
f : ι → ι'
g : ι' → A
hs : AlgebraicIndependent R fun x => g (f ↑x)
⊢ AlgebraicIndependent R fun x => g ↑x
nontriviality R
ι✝ : Type ?u.747618
ι'✝ : Type ?u.747621
R : Type u_3
K : Type ?u.747627
A : Type u_4
A' : Type ?u.747633
A'' : Type ?u.747636
V : Type u
V' : Type ?u.747641
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
ι' : Type u_2
s : Set ι
f : ι → ι'
g : ι' → A
hs : AlgebraicIndependent R fun x => g (f ↑x)
✝ : Nontrivial R
this : InjOn f s
⊢ AlgebraicIndependent R fun x => g ↑x
ι✝ : Type ?u.747618
ι'✝ : Type ?u.747621
R : Type u_3
K : Type ?u.747627
A : Type u_4
A' : Type ?u.747633
A'' : Type ?u.747636
V : Type u
V' : Type ?u.747641
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
ι' : Type u_2
s : Set ι
f : ι → ι'
g : ι' → A
hs : AlgebraicIndependent R fun x => g (f ↑x)
✝ : Nontrivial R
⊢ AlgebraicIndependent R fun x => g ↑x
have : InjOn f s := injOn_iff_injective.2 hs.injective.of_comp
no goals
ι✝ : Type ?u.747618
ι'✝ : Type ?u.747621
R : Type u_3
K : Type ?u.747627
A : Type u_4
A' : Type ?u.747633
A'' : Type ?u.747636
V : Type u
V' : Type ?u.747641
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
ι' : Type u_2
s : Set ι
f : ι → ι'
g : ι' → A
hs : AlgebraicIndependent R fun x => g (f ↑x)
✝ : Nontrivial R
this : InjOn f s
⊢ AlgebraicIndependent R fun x => g ↑x
exact (algebraicIndependent_equiv' (Equiv.Set.imageOfInjOn f s this) rfl).1 hs