This repository was archived by the owner on Jul 24, 2024. It is now read-only.

This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Remove `has_coe_to_fun` instance for `unitary_group` #15749

Open

Labels

good-first-project

opened

on Jul 29, 2022

As discussed here having a has_coe_to_fun instance for the unitary group is not ideal.

to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Assignees

No one assigned

Labels

good-first-project

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests