Theorem TopModuleCat.freeMap_map

Modification history

2026-05-01 00:39
Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean
chore(Topology/Category): replace `TopCat` by `TopCat.{u}` (#38779) …
Modified TopModuleCat.freeMap_mapView on Github →
2025-05-17 13:59
Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean
feat(Algebra/Category): the category of topological modules (#23490)
Added TopModuleCat.freeMap_mapView on Github →