Skip to content

Commit

Permalink
fix(algebra/algebra/restrict_scalars): Remove a bad instance (#8732)
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
eric-wieser committed Aug 18, 2021
1 parent c0f16d2 commit 83c7821
Showing 1 changed file with 0 additions and 8 deletions.
8 changes: 0 additions & 8 deletions src/algebra/algebra/restrict_scalars.lean
Expand Up @@ -107,14 +107,6 @@ rfl
instance : is_scalar_tower R S (restrict_scalars R S M) :=
⟨λ r S M, by { rw [algebra.smul_def, mul_smul], refl }⟩

instance submodule.restricted_module (V : submodule S M) :
module R V :=
restrict_scalars.module R S V

instance submodule.restricted_module_is_scalar_tower (V : submodule S M) :
is_scalar_tower R S V :=
restrict_scalars.is_scalar_tower R S V

end module

section algebra
Expand Down

0 comments on commit 83c7821

Please sign in to comment.