Theorem TopModuleCat.hom_zero_apply

Modification history

2026-06-10 03:47
Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean
feat(Topology/Algebra): use `Is*Apply` for `ContinuousLinearMap` (#39637) …
Modified TopModuleCat.hom_zero_applyView 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.hom_zero_applyView on Github →