Def CompHausLike.cartesianMonoidalCategory

Modification history

2025-11-24 05:14

Mathlib/Topology/Category/CompHausLike/Cartesian.lean

feat(Condensed): cartesian monoidal functor LightProfinite -> LightCondSet (#30800)

Added CompHausLike.cartesianMonoidalCategory View on Github →