Commit 2023-11-20 19:06 9a4ae4a9

View on Github →

chore: add some Unique instances (#8500) The aim is to remove some extraneous Nonempty assumptions in Algebra/DirectLimit.

Estimated changes

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

modified def ModuleCat.directLimitIsColimit

Modified Mathlib/Algebra/DirectLimit.lean

modified theorem AddCommGroup.DirectLimit.lift_unique

modified theorem Module.DirectLimit.lift_unique

modified theorem Ring.DirectLimit.lift_unique

Modified Mathlib/Algebra/Group/TypeTags.lean

Modified Mathlib/Data/Multiset/Basic.lean

Modified Mathlib/Data/Quot.lean

Modified Mathlib/GroupTheory/Abelianization.lean

Modified Mathlib/GroupTheory/FreeAbelianGroup.lean

Modified Mathlib/GroupTheory/FreeGroup/Basic.lean

Modified Mathlib/LinearAlgebra/TensorProduct.lean

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean