Mathlib v3 is deprecated. Go to Mathlib v4

Theorem Module.free.ε_apply

Modification history

2022-07-01 04:21

src/algebra/category/Module/adjunctions.lean

feat(algebra/category/Module): upgrade `free : Type ⥤ Module R` to a monoidal functor (#14328)

Added Module.free.ε_apply View on Github →