Commit 2023-05-10 07:14 9a910f6a

View on Github →

feat: port Topology.Category.Profinite.AsLimit (#3875)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Category/Profinite/AsLimit.lean

added def Profinite.asLimit

added def Profinite.asLimitCone

added def Profinite.asLimitConeIso

added def Profinite.fintypeDiagram

added def Profinite.isoAsLimitConeLift

added def Profinite.lim