ι : Type u_1
ι' : Type ?u.1411198
R : Type ?u.1411201
K : Type u_3
A : Type u_2
A' : Type ?u.1411210
A'' : Type ?u.1411213
V : Type u
V' : Type ?u.1411218
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
inst✝³ : Field K
inst✝² : Algebra K A
inst✝¹ : IsEmpty ι
inst✝ : Nontrivial A
⊢ Injective ↑(algebraMap K A)
ι : Type u_1
ι' : Type ?u.1411198
R : Type ?u.1411201
K : Type u_3
A : Type u_2
A' : Type ?u.1411210
A'' : Type ?u.1411213
V : Type u
V' : Type ?u.1411218
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
inst✝³ : Field K
inst✝² : Algebra K A
inst✝¹ : IsEmpty ι
inst✝ : Nontrivial A
⊢ AlgebraicIndependent K x
rw [algebraicIndependent_empty_type_iff]
no goals
ι : Type u_1
ι' : Type ?u.1411198
R : Type ?u.1411201
K : Type u_3
A : Type u_2
A' : Type ?u.1411210
A'' : Type ?u.1411213
V : Type u
V' : Type ?u.1411218
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
inst✝³ : Field K
inst✝² : Algebra K A
inst✝¹ : IsEmpty ι
inst✝ : Nontrivial A
⊢ Injective ↑(algebraMap K A)
exact RingHom.injective _