Commit 2025-02-05 23:58 c63d2424

View on Github →

refactor(MeasureTheory): ConcreteCategory instance for MeasCat (#21468) Upgrade the HasForget instance on MeasCat to a ConcreteCategory.

Estimated changes

deleted def MeasCat.of
added structure MeasCat
deleted def MeasCat