Commit 2023-05-18 10:53 cb493056

View on Github →

feat: port Topology.Category.TopCommRingCat (#3975)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Category/TopCommRingCat.lean

added theorem TopCommRingCat.coe_of

added def TopCommRingCat.of

added structure TopCommRingCat