Commit 2023-07-07 05:32 811ee339

View on Github →

feat: port Algebra.Category.Algebra.Limits (#5716)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/AlgebraCat/Basic.lean

Created Mathlib/Algebra/Category/AlgebraCat/Limits.lean

added def AlgebraCat.HasLimits.limitCone

added def AlgebraCat.HasLimits.limitConeIsLimit

added theorem AlgebraCat.hasLimitsOfSize

added def AlgebraCat.limitπAlgHom

added def AlgebraCat.sectionsSubalgebra

Modified Mathlib/Algebra/Category/ModuleCat/Limits.lean