English
If M is IsTorsionBySet by I, then for any S with SMul S R and SMul S M and IsScalarTower S R M and IsScalarTower S R R, we have IsScalarTower S (R ⧸ I) M.
Русский
Если M является IsTorsionBySet по I, то при наличии S с действиями над R и M и условий IsScalarTower, т. е. IsScalarTower S (R/I) M, выполняется.
LaTeX
$$$IsScalarTower\\; S\\; (R \\!/ I)\\; M$$$
Lean4
instance isScalarTower [I.IsTwoSided] (hM : IsTorsionBySet R M I) {S : Type*} [SMul S R] [SMul S M]
[IsScalarTower S R M] [IsScalarTower S R R] : @IsScalarTower S (R ⧸ I) M _ (IsTorsionBySet.module hM).toSMul _ :=
-- Porting note: still needed to be fed the Module R / I M instance
@IsScalarTower.mk S (R ⧸ I) M _ (IsTorsionBySet.module hM).toSMul _
(fun b d x => Quotient.inductionOn' d fun c => (smul_assoc b c x :))
