[Merged by Bors] - feat(Algebra/Category/Grp/LargeColimits): large colimits in the category of commutative additive groups#20522

Closed

smorel394 wants to merge 21 commits intomasterfrom SM.bigColimit

+89-1

Commits on Jan 6, 2025

initial commit
morel
committed
Merge remote-tracking branch 'origin' into SM.bigColimit
morel
committed
initial commit
morel
committed
add second lemma
morel
committed
doc string
morel
committed
remove duplicate declarations
morel
committed
update Mathlib.lean
morel
committed
remove unnecessary imports
morel
committed
add import
morel
committed

Commits on Jan 7, 2025

Merge remote-tracking branch 'origin' into SM.bigColimit
morel
committed
finish merge
morel
committed
name change
morel
committed

Commits on Jan 8, 2025

shorten proof
morel
committed
apply suggestions
morel
committed

Commits on Jan 9, 2025

merge
morel
committed
Merge remote-tracking branch 'origin' into SM.bigColimit
morel
committed

Commits on Jan 20, 2025

Merge remote-tracking branch 'origin' into SM.bigColimit
morel
committed
Update Mathlib/Algebra/Category/Grp/LargeColimits.lean

smorel394
and
joelriou
authored
add lemma
morel
committed
Merge branch 'SM.bigColimit' of https://github.com/leanprover-community/mathlib4 into SM.bigColimit
morel
committed
small fix
morel
committed