Theorems · Theorem · category theory

ModuleCat.smul_restrictScalars

∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) (r : R) (M : ModuleCat S),
  ((ModuleCat.restrictScalars f).obj M).smul r = M.smul (f r)

Defined in

Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Cited by

0 results in Mathlib

Foundations

Depth 35 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingRing