mathlib
3a997b1d - fix(group_theory/subgroup): Fix doubly-namespaced instance (#5378)

Commit

5 years ago

fix(group_theory/subgroup): Fix doubly-namespaced instance (#5378) Not sure why the linter missed this.

Author

eric-wieser

Parents