mathlib3
83c78217 - fix(algebra/algebra/restrict_scalars): Remove a bad instance (#8732)

Commit
4 years ago
fix(algebra/algebra/restrict_scalars): Remove a bad instance (#8732) This instance forms a non-defeq diamond with the following one ```lean instance submodule.restricted_module' [module R M] [is_scalar_tower R S M] (V : submodule S M) : module R V := by apply_instance ``` The `submodule.restricted_module_is_scalar_tower` instance is harmless, but it can't exist without the first one so we remove it too. Based on the CI result, this instance wasn't used anyway.
Author
Parents
Loading