Commit 2023-07-08 11:26 59623b0d

View on Github →

feat: API about Small modules (#5769)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Logic/Small/Module.lean

added def algEquivShrink

added def linearEquivShrink