Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-18 06:53 41e152f3

View on Github →

fix(algebra/algebra/tower): remove subalgebra.res which duplicates subalgebra.restrict_scalars (#9251) We use the name restrict_scalars everywhere else, so I kept that one instead of res. res was here first, but the duplicate was added by #7949 presumably because the res name wasn't discoverable.

Estimated changes