mathlib
dd4590af - refactor(algebra/restrict_scalars): remove global instance on module_orig (#13759)

Commit
3 years ago
refactor(algebra/restrict_scalars): remove global instance on module_orig (#13759) The global instance was conceptually wrong, unnecessary (after avoiding a hack in algebra/lie/base_change.lean), and wreaking havoc in #13713. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Author
Parents
Loading