Mathlib v3 is deprecated. Go to Mathlib v4

Theorem category_theory.Module.restrict_scalars.map_apply

Modification history

2022-08-10 17:41

src/algebra/category/Module/change_of_rings.lean

feat(algebra/category/Module/change_of_rings): restriction of scalars (#15672) …

Added category_theory.Module.restrict_scalars.map_apply View on Github →