R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R (AddMonoidAlgebra R M)
⊢ AddMonoid.FG M
R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ FiniteType R (AddMonoidAlgebra R M) ↔ AddMonoid.FG M
refine' ⟨fun h => _, fun h => @AddMonoidAlgebra.finiteType_of_fg _ _ _ _ h⟩
case intro
R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R (AddMonoidAlgebra R M)
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
⊢ AddMonoid.FG M
R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R (AddMonoidAlgebra R M)
⊢ AddMonoid.FG M
obtain ⟨S, hS⟩ := @exists_finset_adjoin_eq_top R M _ _ h
case intro
R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R (AddMonoidAlgebra R M)
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
⊢ m ∈ closure ↑S
case intro
R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R (AddMonoidAlgebra R M)
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
⊢ AddMonoid.FG M
refine' AddMonoid.fg_def.2 ⟨S, (eq_top_iff' _).2 fun m => _⟩
case intro
R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R (AddMonoidAlgebra R M)
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
hm : of' R M m ∈ ↑Subalgebra.toSubmodule (adjoin R (of' R M '' ↑S))
⊢ m ∈ closure ↑S
case intro
R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R (AddMonoidAlgebra R M)
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
⊢ m ∈ closure ↑S
have hm : of' R M m ∈ Subalgebra.toSubmodule (adjoin R (of' R M '' ↑S)) := by
  simp only [hS, top_toSubmodule, Submodule.mem_top]
case intro
R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R (AddMonoidAlgebra R M)
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
hm : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' ↑S))
⊢ m ∈ closure ↑S
case intro
R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R (AddMonoidAlgebra R M)
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
hm : of' R M m ∈ ↑Subalgebra.toSubmodule (adjoin R (of' R M '' ↑S))
⊢ m ∈ closure ↑S
rw [adjoin_eq_span] at hm
no goals
case intro
R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R (AddMonoidAlgebra R M)
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
hm : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' ↑S))
⊢ m ∈ closure ↑S
exact mem_closure_of_mem_span_closure hm
no goals
R : Type u_1
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : FiniteType R (AddMonoidAlgebra R M)
S : Finset M
hS : adjoin R (of' R M '' ↑S) = ⊤
m : M
⊢ of' R M m ∈ ↑Subalgebra.toSubmodule (adjoin R (of' R M '' ↑S))
simp only [hS, top_toSubmodule, Submodule.mem_top]