case mp
R : Type u_1
A : Type u
B : Type ?u.54036
M : Type ?u.54039
N : Type ?u.54042
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
⊢ FiniteType R A → ∃ n f, Surjective ↑f

case mpr
R : Type u_1
A : Type u
B : Type ?u.54036
M : Type ?u.54039
N : Type ?u.54042
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
⊢ (∃ n f, Surjective ↑f) → FiniteType R A
R : Type u_1
A : Type u
B : Type ?u.54036
M : Type ?u.54039
N : Type ?u.54042
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
⊢ FiniteType R A ↔ ∃ n f, Surjective ↑f
constructor
case mp
R : Type u_1
A : Type u
B : Type ?u.54036
M : Type ?u.54039
N : Type ?u.54042
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
⊢ (∃ ι x f, Surjective ↑f) → ∃ n f, Surjective ↑f
case mp
R : Type u_1
A : Type u
B : Type ?u.54036
M : Type ?u.54039
N : Type ?u.54042
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
⊢ FiniteType R A → ∃ n f, Surjective ↑f
rw [iff_quotient_mvPolynomial']
case mp.intro.intro.intro
R : Type u_1
A : Type u
B : Type ?u.54036
M : Type ?u.54039
N : Type ?u.54042
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
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hsur : Surjective ↑f
⊢ ∃ n f, Surjective ↑f
case mp
R : Type u_1
A : Type u
B : Type ?u.54036
M : Type ?u.54039
N : Type ?u.54042
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
⊢ (∃ ι x f, Surjective ↑f) → ∃ n f, Surjective ↑f
rintro ⟨ι, hfintype, ⟨f, hsur⟩⟩
case mp.intro.intro.intro
R : Type u_1
A : Type u
B : Type ?u.54036
M : Type ?u.54039
N : Type ?u.54042
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
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hsur : Surjective ↑f
equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R
⊢ ∃ n f, Surjective ↑f
case mp.intro.intro.intro
R : Type u_1
A : Type u
B : Type ?u.54036
M : Type ?u.54039
N : Type ?u.54042
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
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hsur : Surjective ↑f
⊢ ∃ n f, Surjective ↑f
have equiv := MvPolynomial.renameEquiv R (Fintype.equivFin ι)
no goals
case mp.intro.intro.intro
R : Type u_1
A : Type u
B : Type ?u.54036
M : Type ?u.54039
N : Type ?u.54042
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
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hsur : Surjective ↑f
equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R
⊢ ∃ n f, Surjective ↑f
exact ⟨Fintype.card ι, AlgHom.comp f equiv.symm.toAlgHom, by simpa using hsur⟩
no goals
R : Type u_1
A : Type u
B : Type ?u.54036
M : Type ?u.54039
N : Type ?u.54042
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
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hsur : Surjective ↑f
equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R
⊢ Surjective ↑(AlgHom.comp f ↑(AlgEquiv.symm equiv))
simpa using hsur
case mpr.intro.intro
R : Type u_1
A : Type u
B : Type ?u.54036
M : Type ?u.54039
N : Type ?u.54042
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
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsur : Surjective ↑f
⊢ FiniteType R A
case mpr
R : Type u_1
A : Type u
B : Type ?u.54036
M : Type ?u.54039
N : Type ?u.54042
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
⊢ (∃ n f, Surjective ↑f) → FiniteType R A
rintro ⟨n, ⟨f, hsur⟩⟩
no goals
case mpr.intro.intro
R : Type u_1
A : Type u
B : Type ?u.54036
M : Type ?u.54039
N : Type ?u.54042
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
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsur : Surjective ↑f
⊢ FiniteType R A
exact FiniteType.of_surjective (FiniteType.mvPolynomial R (Fin n)) f hsur