case intro
R : Type u_2
A : Type u
B : Type ?u.10616
M : Type ?u.10619
N : Type ?u.10622
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
val✝ : Fintype ι
⊢ FiniteType R (MvPolynomial ι R)
R : Type u_2
A : Type u
B : Type ?u.10616
M : Type ?u.10619
N : Type ?u.10622
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
⊢ FiniteType R (MvPolynomial ι R)
cases nonempty_fintype ι
no goals
case intro
R : Type u_2
A : Type u
B : Type ?u.10616
M : Type ?u.10619
N : Type ?u.10622
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
val✝ : Fintype ι
⊢ FiniteType R (MvPolynomial ι R)
exact
  ⟨⟨Finset.univ.image MvPolynomial.X, by
      rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
      exact MvPolynomial.adjoin_range_X⟩⟩
R : Type u_2
A : Type u
B : Type ?u.10616
M : Type ?u.10619
N : Type ?u.10622
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
val✝ : Fintype ι
⊢ adjoin R (Set.range MvPolynomial.X) = ⊤
R : Type u_2
A : Type u
B : Type ?u.10616
M : Type ?u.10619
N : Type ?u.10622
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
val✝ : Fintype ι
⊢ adjoin R ↑(Finset.image MvPolynomial.X Finset.univ) = ⊤
rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
no goals
R : Type u_2
A : Type u
B : Type ?u.10616
M : Type ?u.10619
N : Type ?u.10622
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_1
inst✝ : Finite ι
val✝ : Fintype ι
⊢ adjoin R (Set.range MvPolynomial.X) = ⊤
exact MvPolynomial.adjoin_range_X