ι : Type u_1
ι' : Type ?u.148441
R : Type u_2
K : Type ?u.148447
A : Type u_3
A' : Type ?u.148453
A'' : Type ?u.148456
V : Type u
V' : Type ?u.148461
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
⊢ Injective ↑(Finsupp.total ι A R x)
ι : Type u_1
ι' : Type ?u.148441
R : Type u_2
K : Type ?u.148447
A : Type u_3
A' : Type ?u.148453
A'' : Type ?u.148456
V : Type u
V' : Type ?u.148461
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
⊢ LinearIndependent R x
rw [linearIndependent_iff_injective_total]
ι : Type u_1
ι' : Type ?u.148441
R : Type u_2
K : Type ?u.148447
A : Type u_3
A' : Type ?u.148453
A'' : Type ?u.148456
V : Type u
V' : Type ?u.148461
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
this : Finsupp.total ι A R x = LinearMap.comp (AlgHom.toLinearMap (aeval x)) (Finsupp.total ι (MvPolynomial ι R) R X)
⊢ Injective ↑(Finsupp.total ι A R x)
ι : Type u_1
ι' : Type ?u.148441
R : Type u_2
K : Type ?u.148447
A : Type u_3
A' : Type ?u.148453
A'' : Type ?u.148456
V : Type u
V' : Type ?u.148461
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
⊢ Injective ↑(Finsupp.total ι A R x)
have : Finsupp.total ι A R x =
    (MvPolynomial.aeval x).toLinearMap.comp (Finsupp.total ι _ R X) := by
  ext
  simp
ι : Type u_1
ι' : Type ?u.148441
R : Type u_2
K : Type ?u.148447
A : Type u_3
A' : Type ?u.148453
A'' : Type ?u.148456
V : Type u
V' : Type ?u.148461
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
this : Finsupp.total ι A R x = LinearMap.comp (AlgHom.toLinearMap (aeval x)) (Finsupp.total ι (MvPolynomial ι R) R X)
⊢ Injective ↑(LinearMap.comp (AlgHom.toLinearMap (aeval x)) (Finsupp.total ι (MvPolynomial ι R) R X))
ι : Type u_1
ι' : Type ?u.148441
R : Type u_2
K : Type ?u.148447
A : Type u_3
A' : Type ?u.148453
A'' : Type ?u.148456
V : Type u
V' : Type ?u.148461
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
this : Finsupp.total ι A R x = LinearMap.comp (AlgHom.toLinearMap (aeval x)) (Finsupp.total ι (MvPolynomial ι R) R X)
⊢ Injective ↑(Finsupp.total ι A R x)
rw [this]
ι : Type u_1
ι' : Type ?u.148441
R : Type u_2
K : Type ?u.148447
A : Type u_3
A' : Type ?u.148453
A'' : Type ?u.148456
V : Type u
V' : Type ?u.148461
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
this : Finsupp.total ι A R x = LinearMap.comp (AlgHom.toLinearMap (aeval x)) (Finsupp.total ι (MvPolynomial ι R) R X)
⊢ Injective fun x => ↑(Finsupp.total ι (MvPolynomial ι R) R X) x
ι : Type u_1
ι' : Type ?u.148441
R : Type u_2
K : Type ?u.148447
A : Type u_3
A' : Type ?u.148453
A'' : Type ?u.148456
V : Type u
V' : Type ?u.148461
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
this : Finsupp.total ι A R x = LinearMap.comp (AlgHom.toLinearMap (aeval x)) (Finsupp.total ι (MvPolynomial ι R) R X)
⊢ Injective ↑(LinearMap.comp (AlgHom.toLinearMap (aeval x)) (Finsupp.total ι (MvPolynomial ι R) R X))
refine' hx.comp _
ι : Type u_1
ι' : Type ?u.148441
R : Type u_2
K : Type ?u.148447
A : Type u_3
A' : Type ?u.148453
A'' : Type ?u.148456
V : Type u
V' : Type ?u.148461
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
this : Finsupp.total ι A R x = LinearMap.comp (AlgHom.toLinearMap (aeval x)) (Finsupp.total ι (MvPolynomial ι R) R X)
⊢ LinearIndependent R X
ι : Type u_1
ι' : Type ?u.148441
R : Type u_2
K : Type ?u.148447
A : Type u_3
A' : Type ?u.148453
A'' : Type ?u.148456
V : Type u
V' : Type ?u.148461
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
this : Finsupp.total ι A R x = LinearMap.comp (AlgHom.toLinearMap (aeval x)) (Finsupp.total ι (MvPolynomial ι R) R X)
⊢ Injective fun x => ↑(Finsupp.total ι (MvPolynomial ι R) R X) x
rw [← linearIndependent_iff_injective_total]
no goals
ι : Type u_1
ι' : Type ?u.148441
R : Type u_2
K : Type ?u.148447
A : Type u_3
A' : Type ?u.148453
A'' : Type ?u.148456
V : Type u
V' : Type ?u.148461
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
this : Finsupp.total ι A R x = LinearMap.comp (AlgHom.toLinearMap (aeval x)) (Finsupp.total ι (MvPolynomial ι R) R X)
⊢ LinearIndependent R X
exact linearIndependent_X _ _
case h.h
ι : Type u_1
ι' : Type ?u.148441
R : Type u_2
K : Type ?u.148447
A : Type u_3
A' : Type ?u.148453
A'' : Type ?u.148456
V : Type u
V' : Type ?u.148461
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
a✝ : ι
⊢ ↑(LinearMap.comp (Finsupp.total ι A R x) (Finsupp.lsingle a✝)) 1 =
    ↑(LinearMap.comp (LinearMap.comp (AlgHom.toLinearMap (aeval x)) (Finsupp.total ι (MvPolynomial ι R) R X))
          (Finsupp.lsingle a✝))
      1
ι : Type u_1
ι' : Type ?u.148441
R : Type u_2
K : Type ?u.148447
A : Type u_3
A' : Type ?u.148453
A'' : Type ?u.148456
V : Type u
V' : Type ?u.148461
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
⊢ Finsupp.total ι A R x = LinearMap.comp (AlgHom.toLinearMap (aeval x)) (Finsupp.total ι (MvPolynomial ι R) R X)
ext
no goals
case h.h
ι : Type u_1
ι' : Type ?u.148441
R : Type u_2
K : Type ?u.148447
A : Type u_3
A' : Type ?u.148453
A'' : Type ?u.148456
V : Type u
V' : Type ?u.148461
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
a✝ : ι
⊢ ↑(LinearMap.comp (Finsupp.total ι A R x) (Finsupp.lsingle a✝)) 1 =
    ↑(LinearMap.comp (LinearMap.comp (AlgHom.toLinearMap (aeval x)) (Finsupp.total ι (MvPolynomial ι R) R X))
          (Finsupp.lsingle a✝))
      1
simp