Theorems · Theorem · category theory

ModuleCat.smul_naturality

∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} (f : M ⟶ N) (r : R),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).map f) (N.smul r) =
    CategoryTheory.CategoryStruct.comp (M.smul r) ((CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).map f)

Defined in

Mathlib.Algebra.Category.ModuleCat.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

Ring