mathlib
41e152f3 - fix(algebra/algebra/tower): remove `subalgebra.res` which duplicates `subalgebra.restrict_scalars` (#9251)

Commit
4 years ago
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.
Author
Parents
Loading