Documentation

Mathlib.Topology.Category.LightProfinite.Cartesian

Cartesian monoidal structure on LightProfinite #

This file defines the cartesian monoidal structure on LightProfinite given by the type-theoretic product.

source
instance LightProfinite.instCartesianMonoidalCategory :
CategoryTheory.CartesianMonoidalCategory LightProfinite
Equations