Def algEquivShrink

Modification history

2026-01-15 12:34
Mathlib/Algebra/Algebra/Shrink.lean
chore: remove declarations deprecated between 2021-01-15 and 2025-07-15 (#33988) …
Deleted algEquivShrinkView on Github →
2025-07-11 19:04
Mathlib/Algebra/Algebra/Shrink.lean
chore(Algebra/Equiv/TransferInstance): delete duplicated `Shrink` material (#26774) …
Modified algEquivShrinkView on Github →
2023-07-08 11:26
Mathlib/Logic/Small/Module.lean
feat: API about Small modules (#5769)
Added algEquivShrinkView on Github →