feat: port RingTheory.Finiteness (#2811)

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Matthew Ballard <matt@mrb.email> Co-authored-by: Johan Commelin <johan@commelin.net>
leanprover-community · Mar 18, 2023 · e5ec18f · e5ec18f
1 parent 161857d
commit e5ec18f
Show file tree

Hide file tree

Showing 3 changed files with 775 additions and 1 deletion.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1268,6 +1268,7 @@ import Mathlib.RingTheory.Congruence
 import Mathlib.RingTheory.Coprime.Basic
 import Mathlib.RingTheory.Coprime.Ideal
 import Mathlib.RingTheory.Coprime.Lemmas
+import Mathlib.RingTheory.Finiteness
 import Mathlib.RingTheory.Fintype
 import Mathlib.RingTheory.FreeRing
 import Mathlib.RingTheory.Ideal.Basic

diff --git a/Mathlib/Algebra/Algebra/RestrictScalars.lean b/Mathlib/Algebra/Algebra/RestrictScalars.lean
@@ -113,10 +113,11 @@ instance [Module S M] : Module R (RestrictScalars R S M) :=
 
 /-- This instance is only relevant when `RestrictScalars.moduleOrig` is available as an instance.
 -/
-instance [Module S M] : IsScalarTower R S (RestrictScalars R S M) :=
+instance RestrictScalars.isScalarTower [Module S M] : IsScalarTower R S (RestrictScalars R S M) :=
   ⟨fun r S M ↦ by
     rw [Algebra.smul_def, mul_smul]
     rfl⟩
+#align restrict_scalars.is_scalar_tower RestrictScalars.isScalarTower
 
 end