chore: split Algebra.Group.Nat (#19375)

Mathlib.lean

@@ -281,7 +281,10 @@ import Mathlib.Algebra.Group.Int
 import Mathlib.Algebra.Group.Invertible.Basic
 import Mathlib.Algebra.Group.Invertible.Defs
 import Mathlib.Algebra.Group.MinimalAxioms
-import Mathlib.Algebra.Group.Nat
+import Mathlib.Algebra.Group.Nat.Basic
+import Mathlib.Algebra.Group.Nat.Even
+import Mathlib.Algebra.Group.Nat.TypeTags
+import Mathlib.Algebra.Group.Nat.Units
 import Mathlib.Algebra.Group.NatPowAssoc
 import Mathlib.Algebra.Group.Opposite
 import Mathlib.Algebra.Group.PNatPowAssoc

Mathlib/Algebra/Group/Int.lean

@@ -3,7 +3,8 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 -/
-import Mathlib.Algebra.Group.Nat
+import Mathlib.Algebra.Group.Nat.Even
+import Mathlib.Algebra.Group.Nat.Units
 import Mathlib.Algebra.Group.Units.Basic
 import Mathlib.Data.Int.Sqrt
 

Mathlib/Algebra/Group/Nat/Basic.lean

@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2014 Floris van Doorn (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
+-/
+import Mathlib.Algebra.Group.Defs
+
+/-!
+# The natural numbers form a monoid
+
+This file contains the additive and multiplicative monoid instances on the natural numbers.
+
+See note [foundational algebra order theory].
+-/
+
+assert_not_exists MonoidWithZero
+assert_not_exists DenselyOrdered
+
+namespace Nat
+
+/-! ### Instances -/
+
+instance instAddCancelCommMonoid : AddCancelCommMonoid ℕ where
+  add := Nat.add
+  add_assoc := Nat.add_assoc
+  zero := Nat.zero
+  zero_add := Nat.zero_add
+  add_zero := Nat.add_zero
+  add_comm := Nat.add_comm
+  nsmul m n := m * n
+  nsmul_zero := Nat.zero_mul
+  nsmul_succ := succ_mul
+  add_left_cancel _ _ _ := Nat.add_left_cancel
+
+instance instCommMonoid : CommMonoid ℕ where
+  mul := Nat.mul
+  mul_assoc := Nat.mul_assoc
+  one := Nat.succ Nat.zero
+  one_mul := Nat.one_mul
+  mul_one := Nat.mul_one
+  mul_comm := Nat.mul_comm
+  npow m n := n ^ m
+  npow_zero := Nat.pow_zero
+  npow_succ _ _ := rfl
+
+/-!
+### Extra instances to short-circuit type class resolution
+
+These also prevent non-computable instances being used to construct these instances non-computably.
+-/
+
+instance instAddCommMonoid    : AddCommMonoid ℕ    := by infer_instance
+instance instAddMonoid        : AddMonoid ℕ        := by infer_instance
+instance instMonoid           : Monoid ℕ           := by infer_instance
+instance instCommSemigroup    : CommSemigroup ℕ    := by infer_instance
+instance instSemigroup        : Semigroup ℕ        := by infer_instance
+instance instAddCommSemigroup : AddCommSemigroup ℕ := by infer_instance
+instance instAddSemigroup     : AddSemigroup ℕ     := by infer_instance
+
+/-! ### Miscellaneous lemmas -/
+
+-- We set the simp priority slightly lower than default; later more general lemmas will replace it.
+@[simp 900] protected lemma nsmul_eq_mul (m n : ℕ) : m • n = m * n := rfl
+
+end Nat

Mathlib/Algebra/Group/Nat.lean → Mathlib/Algebra/Group/Nat/Even.lean

@@ -4,76 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 import Mathlib.Algebra.Group.Even
-import Mathlib.Algebra.Group.Units.Defs
+import Mathlib.Algebra.Group.Nat.Basic
 import Mathlib.Data.Nat.Sqrt
 
 /-!
-# The natural numbers form a monoid
-
-This file contains the additive and multiplicative monoid instances on the natural numbers.
-
-See note [foundational algebra order theory].
+# `IsSquare` and `Even` for natural numbers
 -/
 
 assert_not_exists MonoidWithZero
 assert_not_exists DenselyOrdered
 
-open Multiplicative
-
 namespace Nat
 
-/-! ### Instances -/
-
-instance instAddCancelCommMonoid : AddCancelCommMonoid ℕ where
-  add := Nat.add
-  add_assoc := Nat.add_assoc
-  zero := Nat.zero
-  zero_add := Nat.zero_add
-  add_zero := Nat.add_zero
-  add_comm := Nat.add_comm
-  nsmul m n := m * n
-  nsmul_zero := Nat.zero_mul
-  nsmul_succ := succ_mul
-  add_left_cancel _ _ _ := Nat.add_left_cancel
-
-instance instCommMonoid : CommMonoid ℕ where
-  mul := Nat.mul
-  mul_assoc := Nat.mul_assoc
-  one := Nat.succ Nat.zero
-  one_mul := Nat.one_mul
-  mul_one := Nat.mul_one
-  mul_comm := Nat.mul_comm
-  npow m n := n ^ m
-  npow_zero := Nat.pow_zero
-  npow_succ _ _ := rfl
-
-/-!
-### Extra instances to short-circuit type class resolution
-
-These also prevent non-computable instances being used to construct these instances non-computably.
--/
-
-instance instAddCommMonoid    : AddCommMonoid ℕ    := by infer_instance
-instance instAddMonoid        : AddMonoid ℕ        := by infer_instance
-instance instMonoid           : Monoid ℕ           := by infer_instance
-instance instCommSemigroup    : CommSemigroup ℕ    := by infer_instance
-instance instSemigroup        : Semigroup ℕ        := by infer_instance
-instance instAddCommSemigroup : AddCommSemigroup ℕ := by infer_instance
-instance instAddSemigroup     : AddSemigroup ℕ     := by infer_instance
-
-/-! ### Miscellaneous lemmas -/
-
--- We set the simp priority slightly lower than default; later more general lemmas will replace it.
-@[simp 900] protected lemma nsmul_eq_mul (m n : ℕ) : m • n = m * n := rfl
-
-section Multiplicative
-
-lemma toAdd_pow (a : Multiplicative ℕ) (b : ℕ) : toAdd (a ^ b) = toAdd a * b := mul_comm _ _
-
-@[simp] lemma ofAdd_mul (a b : ℕ) : ofAdd (a * b) = ofAdd a ^ b := (toAdd_pow _ _).symm
-
-end Multiplicative
-
 /-! #### Parity -/
 
 variable {m n : ℕ}
@@ -158,23 +100,4 @@ example (m n : ℕ) (h : Even m) : ¬Even (n + 3) ↔ Even (m ^ 2 + m + n) := by
 -- Porting note: the `simp` lemmas about `bit*` no longer apply.
 example : ¬Even 25394535 := by decide
 
-/-! #### Units -/
-
-lemma units_eq_one (u : ℕˣ) : u = 1 := Units.ext <| Nat.eq_one_of_dvd_one ⟨u.inv, u.val_inv.symm⟩
-
-lemma addUnits_eq_zero (u : AddUnits ℕ) : u = 0 :=
-  AddUnits.ext <| (Nat.eq_zero_of_add_eq_zero u.val_neg).1
-
-@[simp] protected lemma isUnit_iff {n : ℕ} : IsUnit n ↔ n = 1 where
-  mp := by rintro ⟨u, rfl⟩; obtain rfl := Nat.units_eq_one u; rfl
-  mpr h := h.symm ▸ ⟨1, rfl⟩
-
-instance unique_units : Unique ℕˣ where
-  default := 1
-  uniq := Nat.units_eq_one
-
-instance unique_addUnits : Unique (AddUnits ℕ) where
-  default := 0
-  uniq := Nat.addUnits_eq_zero
-
 end Nat

Mathlib/Algebra/Group/Nat/TypeTags.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2014 Floris van Doorn (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
+-/
+import Mathlib.Algebra.Group.Nat.Basic
+import Mathlib.Algebra.Group.TypeTags.Basic
+
+/-!
+# Lemmas about `Multiplicative ℕ`
+-/
+
+assert_not_exists MonoidWithZero
+assert_not_exists DenselyOrdered
+
+open Multiplicative
+
+namespace Nat
+
+lemma toAdd_pow (a : Multiplicative ℕ) (b : ℕ) : toAdd (a ^ b) = toAdd a * b := mul_comm _ _
+
+@[simp] lemma ofAdd_mul (a b : ℕ) : ofAdd (a * b) = ofAdd a ^ b := (toAdd_pow _ _).symm
+
+end Nat

Mathlib/Algebra/Group/Nat/Units.lean

@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2014 Floris van Doorn (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
+-/
+import Mathlib.Algebra.Group.Nat.Basic
+import Mathlib.Algebra.Group.Units.Defs
+import Mathlib.Logic.Unique
+
+/-!
+# The unit of the natural numbers
+-/
+
+assert_not_exists MonoidWithZero
+assert_not_exists DenselyOrdered
+
+namespace Nat
+
+/-! #### Units -/
+
+lemma units_eq_one (u : ℕˣ) : u = 1 := Units.ext <| Nat.eq_one_of_dvd_one ⟨u.inv, u.val_inv.symm⟩
+
+lemma addUnits_eq_zero (u : AddUnits ℕ) : u = 0 :=
+  AddUnits.ext <| (Nat.eq_zero_of_add_eq_zero u.val_neg).1
+
+@[simp] protected lemma isUnit_iff {n : ℕ} : IsUnit n ↔ n = 1 where
+  mp := by rintro ⟨u, rfl⟩; obtain rfl := Nat.units_eq_one u; rfl
+  mpr h := h.symm ▸ ⟨1, rfl⟩
+
+instance unique_units : Unique ℕˣ where
+  default := 1
+  uniq := Nat.units_eq_one
+
+instance unique_addUnits : Unique (AddUnits ℕ) where
+  default := 0
+  uniq := Nat.addUnits_eq_zero
+
+end Nat

Mathlib/Algebra/Group/Submonoid/Operations.lean

@@ -5,9 +5,10 @@ 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
+import Mathlib.Algebra.Group.Nat.Basic
 import Mathlib.Algebra.Group.Prod
 import Mathlib.Algebra.Group.Submonoid.Basic
+import Mathlib.Algebra.Group.TypeTags.Basic
 
 /-!
 # Operations on `Submonoid`s

Mathlib/Algebra/GroupPower/IterateHom.lean

@@ -5,7 +5,6 @@ Authors: Yury Kudryashov
 -/
 import Mathlib.Algebra.Group.Action.Opposite
 import Mathlib.Algebra.Group.Int
-import Mathlib.Algebra.Group.Nat
 import Mathlib.Logic.Function.Iterate
 import Mathlib.Tactic.Common
 

Mathlib/Algebra/Order/Group/Nat.lean

@@ -3,7 +3,7 @@ Copyright (c) 2014 Floris van Doorn (c) 2016 Microsoft Corporation. All rights r
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
-import Mathlib.Algebra.Group.Nat
+import Mathlib.Algebra.Group.Nat.Basic
 import Mathlib.Algebra.Order.Monoid.Canonical.Defs
 import Mathlib.Algebra.Order.Sub.Defs
 import Mathlib.Data.Nat.Defs

Mathlib/Algebra/Order/Ring/Basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2015 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Robert Y. Lewis
 -/
+import Mathlib.Algebra.Group.Nat.Units
 import Mathlib.Algebra.Order.Monoid.Unbundled.Pow
 import Mathlib.Algebra.Order.Ring.Defs
 import Mathlib.Algebra.Ring.Parity

Mathlib/Algebra/Ring/Nat.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 import Mathlib.Algebra.CharZero.Defs
-import Mathlib.Algebra.Group.Nat
+import Mathlib.Algebra.Group.Nat.Basic
 import Mathlib.Algebra.Ring.Defs
 
 /-!
@@ -15,8 +15,6 @@ This file contains the commutative semiring instance on the natural numbers.
 See note [foundational algebra order theory].
 -/
 
-open Multiplicative
-
 namespace Nat
 
 /-! ### Instances -/

Mathlib/Algebra/Ring/Parity.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
+import Mathlib.Algebra.Group.Nat.Even
 import Mathlib.Data.Nat.Cast.Basic
 import Mathlib.Data.Nat.Cast.Commute
 import Mathlib.Data.Set.Operations

Mathlib/Data/List/SplitLengths.lean

@@ -3,8 +3,8 @@ Copyright (c) 2024 Daniel Weber. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Daniel Weber
 -/
+import Mathlib.Algebra.Group.Nat.Basic
 import Mathlib.Order.MinMax
-import Mathlib.Algebra.Group.Nat
 
 /-!
 # Splitting a list to chunks of specified lengths

Mathlib/Data/Multiset/Basic.lean

@@ -3,13 +3,14 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Mathlib.Algebra.Group.Nat
+import Mathlib.Algebra.Group.Hom.Defs
+import Mathlib.Algebra.Group.Nat.Basic
 import Mathlib.Algebra.Order.Sub.Unbundled.Basic
+import Mathlib.Data.List.Perm.Basic
+import Mathlib.Data.List.Perm.Lattice
 import Mathlib.Data.List.Perm.Subperm
 import Mathlib.Data.Set.List
 import Mathlib.Order.Hom.Basic
-import Mathlib.Data.List.Perm.Lattice
-import Mathlib.Data.List.Perm.Basic
 
 /-!
 # Multisets

Mathlib/Data/Nat/Bits.lean

@@ -3,8 +3,7 @@ Copyright (c) 2022 Praneeth Kolichala. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Praneeth Kolichala
 -/
-import Mathlib.Algebra.Group.Basic
-import Mathlib.Algebra.Group.Nat
+import Mathlib.Algebra.Group.Nat.Basic
 import Mathlib.Data.Nat.Defs
 import Mathlib.Data.Nat.BinaryRec
 import Mathlib.Data.List.Defs

Mathlib/Data/Nat/Bitwise.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel, Alex Keizer
 -/
-import Mathlib.Algebra.Group.Units.Basic
+import Mathlib.Algebra.Group.Nat.Even
 import Mathlib.Algebra.NeZero
 import Mathlib.Algebra.Ring.Nat
 import Mathlib.Data.List.GetD

Mathlib/Data/Nat/Cast/Basic.lean

@@ -4,9 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Algebra.Divisibility.Basic
+import Mathlib.Algebra.Group.Even
+import Mathlib.Algebra.Group.TypeTags.Hom
 import Mathlib.Algebra.Ring.Hom.Defs
 import Mathlib.Algebra.Ring.Nat
-import Mathlib.Algebra.Group.TypeTags.Hom
 
 /-!
 # Cast of natural numbers (additional theorems)

Mathlib/Data/Nat/GCD/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura
 -/
 import Batteries.Data.Nat.Gcd
+import Mathlib.Algebra.Group.Nat.Units
 import Mathlib.Algebra.GroupWithZero.Divisibility
 import Mathlib.Algebra.Ring.Nat
 

Mathlib/Data/Nat/PSub.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Algebra.Group.Basic
-import Mathlib.Algebra.Group.Nat
+import Mathlib.Algebra.Group.Nat.Basic
 
 /-!
 # Partial predecessor and partial subtraction on the natural numbers