Merge remote-tracking branch 'alreadydone/jyxu/isscalartower_trans' into isscalartower_trans

Author: xroblot

Mathlib/Algebra/Algebra/Tower.lean

@@ -122,28 +122,6 @@ theorem algebraMap_eq : algebraMap R A = (algebraMap S A).comp (algebraMap R S)
 theorem algebraMap_apply (x : R) : algebraMap R A x = algebraMap S A (algebraMap R S x) := by
   rw [algebraMap_eq R S A, RingHom.comp_apply]
 
-/--
-Let `R ⊆ S ⊆ T ⊆ U` be a tower of rings. If `R ⊆ S ⊆ T`, `R ⊆ T ⊆ U` and `S ⊆ T ⊆ U` are
-scalar towers, then `R ⊆ S ⊆ U` is also a scalar tower.
--/
-theorem trans_left (T U : Type*) [CommSemiring T] [CommSemiring U] [Algebra S T] [Algebra R T]
-    [Algebra T U] [Algebra R U] [Algebra S U] [IsScalarTower R S T] [IsScalarTower R T U]
-    [IsScalarTower S T U] : IsScalarTower R S U := by
-  apply IsScalarTower.of_algebraMap_eq'
-  rw [IsScalarTower.algebraMap_eq S T, RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq,
-    ← IsScalarTower.algebraMap_eq]
-
-/--
-Let `R ⊆ S ⊆ T ⊆ U` be a tower of rings. If `R ⊆ S ⊆ T`, `R ⊆ S ⊆ U` and `S ⊆ T ⊆ U` are
-scalar towers, then `R ⊆ T ⊆ U` is also a scalar tower.
--/
-theorem trans_right (T U : Type*) [CommSemiring T] [CommSemiring U] [Algebra S T] [Algebra R T]
-    [Algebra T U] [Algebra R U] [Algebra S U] [IsScalarTower R S T] [IsScalarTower R S U]
-    [IsScalarTower S T U] : IsScalarTower R T U := by
-  apply IsScalarTower.of_algebraMap_eq'
-  rw [IsScalarTower.algebraMap_eq R S T, ← RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq,
-    ← IsScalarTower.algebraMap_eq]
-
 @[ext]
 theorem Algebra.ext {S : Type u} {A : Type v} [CommSemiring S] [Semiring A] (h1 h2 : Algebra S A)
     (h : ∀ (r : S) (x : A), (by have I := h1; exact r • x) = r • x) : h1 = h2 :=

Mathlib/Algebra/Group/Action/Defs.lean

@@ -488,7 +488,6 @@ lemma isScalarTower_iff_smulCommClass_of_commMonoid (R₁ R : Type*)
     SMulCommClass R₁ R R ↔ IsScalarTower R₁ R R :=
   ⟨fun _ ↦ IsScalarTower.of_commMonoid R₁ R, fun _ ↦ SMulCommClass.of_commMonoid R₁ R R⟩
 
-
 end
 
 section CompatibleScalar
@@ -516,6 +515,16 @@ lemma SMulCommClass.of_mul_smul_one {M N} [Monoid N] [SMul M N]
     (H : ∀ (x : M) (y : N), y * x • (1 : N) = x • y) : SMulCommClass M N N :=
   ⟨fun x y z ↦ by rw [← H x z, smul_eq_mul, ← H, smul_eq_mul, mul_assoc]⟩
 
+@[to_additive] lemma IsScalarTower.trans_left (M N P Q)
+    [SMul M N] [SMul M P] [SMul M Q] [SMul N P] [SMul N Q] [Monoid P] [MulAction P Q]
+    [IsScalarTower M N P] [IsScalarTower M P Q] [IsScalarTower N P Q] : IsScalarTower M N Q where
+  smul_assoc m n q := by rw [← smul_one_smul P, smul_assoc m, smul_assoc, smul_one_smul]
+
+@[to_additive] lemma IsScalarTower.trans_right (M N P Q)
+    [SMul M N] [SMul M P] [SMul M Q] [SMul P Q] [Monoid N] [MulAction N P] [MulAction N Q]
+    [IsScalarTower M N P] [IsScalarTower M N Q] [IsScalarTower N P Q] : IsScalarTower M P Q where
+  smul_assoc m p q := by rw [← smul_one_smul N m, smul_assoc, smul_one_smul]
+
 end CompatibleScalar
 
 /-- Typeclass for multiplicative actions on multiplicative structures.