mathlib3
3b8ae4ca
- Merge branch 'FR_quotient2' into FR_dfinsupp_sigma_uncurry
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
2 years ago
Merge branch 'FR_quotient2' into FR_dfinsupp_sigma_uncurry
References
#18318 - feat(data/dfinsupp/basic): remove decidable typeclass assumptions on `sigma_uncurry`
Author
astrainfinita
Parents
7f407d12
350eb252
Loading