Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-03-13 12:12
b3e1613e
View on Github →
feat: port CategoryTheory.ConnectedComponents (
#2843
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/CategoryTheory/ConnectedComponents.lean
added
def
CategoryTheory.Component.ι
added
def
CategoryTheory.Component
added
def
CategoryTheory.ConnectedComponents
added
def
CategoryTheory.decomposedEquiv
added
def
CategoryTheory.decomposedTo
added
theorem
CategoryTheory.inclusion_comp_decomposedTo