mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard
verified publisher icon leanprover-community

Remove `has_coe_to_fun` instance for `unitary_group`

Open mcdoll opened this issue 3 years ago • 0 comments

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

mcdoll avatar Jul 29 '22 10:07 mcdoll