Zulip Chat Archive

Stream: mathlib4

Topic: Duplicate algebraic instance for `Shrink`

Yury G. Kudryashov (May 01 2025 at 06:00):

We have, e.g., docs#Equiv.instOneShrink and docs#instOneShrink

Yury G. Kudryashov (May 01 2025 at 06:01):

CC: @Kim Morrison

Yury G. Kudryashov (May 01 2025 at 06:13):

(you've authored one of the copies)

Last updated: May 02 2025 at 03:31 UTC