Commit 2025-11-24 05:14 d1de2759

View on Github →

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

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Condensed/Light/Functors.lean

Created Mathlib/Topology/Category/CompHausLike/Cartesian.lean

added def CompHausLike.cartesianMonoidalCategory

added def CompHausLike.productCone

added def CompHausLike.productIsLimit

Created Mathlib/Topology/Category/LightProfinite/Cartesian.lean