mathlib3
b2ab94f8
- fix(group_theory): Remove a duplicate fintype instance on quotient_group.quotient (#5368)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
fix(group_theory): Remove a duplicate fintype instance on quotient_group.quotient (#5368) This noncomputable instance was annoying, and can easy be recovered by passing in a classical decidable_pred instance instead.
Author
eric-wieser
Parents
b364d337
Loading