case intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
⊢ FinitePresentation R (MvPolynomial ι R)
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
ι : Type u_2
inst✝ : Finite ι
⊢ FinitePresentation R (MvPolynomial ι R)
cases nonempty_fintype ι
case intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
eqv : MvPolynomial (Fin (Fintype.card ι)) R ≃ₐ[R] MvPolynomial ι R :=
  AlgEquiv.symm (MvPolynomial.renameEquiv R (Fintype.equivFin ι))
⊢ FinitePresentation R (MvPolynomial ι R)
case intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
⊢ FinitePresentation R (MvPolynomial ι R)
let eqv := (MvPolynomial.renameEquiv R <| Fintype.equivFin ι).symm
no goals
case intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
ι : Type u_2
inst✝ : Finite ι
val✝ : Fintype ι
eqv : MvPolynomial (Fin (Fintype.card ι)) R ≃ₐ[R] MvPolynomial ι R :=
  AlgEquiv.symm (MvPolynomial.renameEquiv R (Fintype.equivFin ι))
⊢ FinitePresentation R (MvPolynomial ι R)
exact
  ⟨Fintype.card ι, eqv, eqv.surjective,
    ((RingHom.injective_iff_ker_eq_bot _).1 eqv.injective).symm ▸ Submodule.fg_bot⟩