mathlib
36c90d5e - fix(algebra/algebra/subalgebra): fix incorrect namespaces and remove duplicate instance (#8140)

Commit
4 years ago
fix(algebra/algebra/subalgebra): fix incorrect namespaces and remove duplicate instance (#8140) We already had a `subsingleton` instance on `alg_hom`s added in #5672, but we didn't find it #8110 because * gh-6025 means we can't ask `apply_instance` to find it * it had an incorrect name in the wrong namespace Code opting into this instance will need to change from ```lean local attribute [instance] alg_hom.subsingleton ``` to ```lean local attribute [instance] alg_hom.subsingleton subalgebra.subsingleton_of_subsingleton ```
Author
Parents
Loading