[Merged by Bors] - refactor(Data/Rat/NNRat): move module and algebra instances

Mathlib/Algebra/Algebra/Basic.lean

@@ -722,6 +722,10 @@ instance algebraRat {α} [DivisionRing α] [CharZero α] : Algebra ℚ α where
   commutes' := Rat.cast_commute
 #align algebra_rat algebraRat
 
+/-- The rational numbers are an algebra over the non-negative rationals. -/
+instance : Algebra NNRat ℚ :=
+  NNRat.coeHom.toAlgebra
+
 /-- The two `Algebra ℚ ℚ` instances should coincide. -/
 example : algebraRat = Algebra.id ℚ :=
   rfl

Mathlib/Algebra/Module/Basic.lean

@@ -5,6 +5,7 @@
 -/
 import Mathlib.Algebra.Function.Indicator
 import Mathlib.Algebra.SMulWithZero
+import Mathlib.Data.Rat.NNRat
 import Mathlib.GroupTheory.GroupAction.Group
 import Mathlib.GroupTheory.GroupAction.Pi
 import Mathlib.Logic.Basic
@@ -473,6 +474,11 @@
   map_rat_cast_smul f ℚ ℚ c x
 #align map_rat_smul map_rat_smul
 
+
+/-- A `Module` over `ℚ` restricts to a `Module` over `ℚ≥0`. -/
+instance [AddCommMonoid α] [Module ℚ α] : Module NNRat α :=
+  Module.compHom α NNRat.coeHom
+
 /-- There can be at most one `Module ℚ E` structure on an additive commutative group. -/
 instance subsingleton_rat_module (E : Type*) [AddCommGroup E] : Subsingleton (Module ℚ E) :=
   ⟨fun P Q => (Module.ext' P Q) fun r x => @map_rat_smul _ _ _ _ P Q _ _ (AddMonoidHom.id E) r x⟩
@@ -841,4 +847,4 @@
 end SMulWithZero
 end Set
 
 assert_not_exists Multiset

Mathlib/Data/Nat/Digits.lean

@@ -9,6 +9,7 @@ import Mathlib.Data.Nat.Log
 import Mathlib.Data.List.BigOperators.Lemmas
 import Mathlib.Data.List.Indexes
 import Mathlib.Data.List.Palindrome
+import Mathlib.Algebra.CharZero.Lemmas
 import Mathlib.Algebra.Parity
 import Mathlib.Algebra.BigOperators.Intervals
 import Mathlib.Tactic.IntervalCases

Mathlib/Data/Rat/NNRat.lean

@@ -3,9 +3,10 @@ Copyright (c) 2022 Yaël Dillies, Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
-import Mathlib.Algebra.Algebra.Basic
+import Mathlib.Algebra.Function.Indicator
 import Mathlib.Algebra.Order.Nonneg.Field
 import Mathlib.Data.Int.Lemmas
+import Mathlib.Data.Rat.Order
 
 #align_import data.rat.nnrat from "leanprover-community/mathlib"@"b3f4f007a962e3787aa0f3b5c7942a1317f7d88e"
 
@@ -28,8 +29,6 @@ of `x` with `↑x`. This tactic also works for a function `f : α → ℚ` with
 
 open Function
 
-open BigOperators
-
 /-- Nonnegative rational numbers. -/
 def NNRat := { q : ℚ // 0 ≤ q } deriving
   CanonicallyOrderedCommSemiring, CanonicallyLinearOrderedSemifield, LinearOrderedCommGroupWithZero,
@@ -215,10 +214,6 @@ theorem mk_coe_nat (n : ℕ) : @Eq ℚ≥0 (⟨(n : ℚ), n.cast_nonneg⟩ : ℚ
   ext (coe_natCast n).symm
 #align nnrat.mk_coe_nat NNRat.mk_coe_nat
 
-/-- The rational numbers are an algebra over the non-negative rationals. -/
-instance : Algebra ℚ≥0 ℚ :=
-  coeHom.toAlgebra
-
 /-- A `MulAction` over `ℚ` restricts to a `MulAction` over `ℚ≥0`. -/
 instance [MulAction ℚ α] : MulAction ℚ≥0 α :=
   MulAction.compHom α coeHom.toMonoidHom
@@ -227,10 +222,6 @@ instance [MulAction ℚ α] : MulAction ℚ≥0 α :=
 instance [AddCommMonoid α] [DistribMulAction ℚ α] : DistribMulAction ℚ≥0 α :=
   DistribMulAction.compHom α coeHom.toMonoidHom
 
-/-- A `Module` over `ℚ` restricts to a `Module` over `ℚ≥0`. -/
-instance [AddCommMonoid α] [Module ℚ α] : Module ℚ≥0 α :=
-  Module.compHom α coeHom
-
 @[simp]
 theorem coe_coeHom : ⇑coeHom = ((↑) : ℚ≥0 → ℚ) :=
   rfl