add

Author: staroperator

Mathlib/Algebra/Group/Submonoid/Membership.lean

@@ -512,3 +512,10 @@ theorem ofAdd_image_multiples_eq_powers_ofAdd [AddMonoid A] {x : A} :
   exact ofMul_image_powers_eq_multiples_ofMul
 
 end mul_add
+
+@[simp] theorem Nat.addSubmonoidClosure_one : AddSubmonoid.closure ({1} : Set ℕ) = ⊤ := by
+  ext
+  simp [AddSubmonoid.mem_closure_singleton]
+
+@[deprecated (since := "2025-08-14")]
+alias Nat.addSubmonoid_closure_one := Nat.addSubmonoidClosure_one

Mathlib/Algebra/Group/Submonoid/Operations.lean

@@ -5,7 +5,6 @@ Authors: Johannes Hölzl, Kenny Lau, Johan Commelin, Mario Carneiro, Kevin Buzza
 Amelia Livingston, Yury Kudryashov
 -/
 import Mathlib.Algebra.Group.Action.Faithful
-import Mathlib.Algebra.Group.Nat.Defs
 import Mathlib.Algebra.Group.Prod
 import Mathlib.Algebra.Group.Submonoid.Basic
 import Mathlib.Algebra.Group.Submonoid.MulAction
@@ -1012,19 +1011,6 @@ end Submonoid
 
 end Units
 
-open AddSubmonoid Set
-
-namespace Nat
-
-@[simp] lemma addSubmonoidClosure_one : closure ({1} : Set ℕ) = ⊤ := by
-  refine (eq_top_iff' _).2 <| Nat.rec (zero_mem _) ?_
-  simp_rw [Nat.succ_eq_add_one]
-  exact fun n hn ↦ AddSubmonoid.add_mem _ hn <| subset_closure <| Set.mem_singleton _
-
-@[deprecated (since := "2025-08-14")] alias addSubmonoid_closure_one := addSubmonoidClosure_one
-
-end Nat
-
 namespace Submonoid
 
 variable {F : Type*} [FunLike F M N] [mc : MonoidHomClass F M N]

Mathlib/Algebra/Order/Star/Basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2023 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
-import Mathlib.Algebra.Group.Submonoid.Operations
+import Mathlib.Algebra.Group.Submonoid.Membership
 import Mathlib.Algebra.GroupWithZero.Regular
 import Mathlib.Algebra.NoZeroSMulDivisors.Defs
 import Mathlib.Algebra.Order.Group.Nat