Def algEquivShrink

Modification history

2025-07-11 19:04

Mathlib/Algebra/Algebra/Shrink.lean

chore(Algebra/Equiv/TransferInstance): delete duplicated `Shrink` material (#26774) …

Modified algEquivShrink View on Github →

2023-07-08 11:26

Mathlib/Logic/Small/Module.lean

feat: API about Small modules (#5769)

Added algEquivShrink View on Github →