basic): remove decidable typeclass assumptions on `sigma_uncurry`
#18318

Open

Commits

feat:(data/*/quot): quotient_lift on a finite family

astrainfinita committed 3 years ago
fix

astrainfinita committed 3 years ago
fix

astrainfinita committed 3 years ago
lint & docs

astrainfinita committed 3 years ago
`Sort`

astrainfinita committed 3 years ago
feat(data/quot): make `trunc` a quotient

astrainfinita committed 3 years ago
Merge branch 'FR_trunc' into FR_dfinsupp_sigma_uncurry

astrainfinita committed 3 years ago
feat(data/dfinsupp/basic): remove some typeclass assumptions on `sigma_uncurry`

astrainfinita committed 3 years ago
fix

astrainfinita committed 3 years ago
docs

astrainfinita committed 3 years ago
Merge branch 'FR_trunc' into FR_dfinsupp_sigma_uncurry

astrainfinita committed 3 years ago
docs

astrainfinita committed 3 years ago
golf

astrainfinita committed 3 years ago
tweak names

astrainfinita committed 3 years ago
fix

astrainfinita committed 3 years ago
golf

astrainfinita committed 3 years ago
use fintype version quotient_lift

astrainfinita committed 3 years ago
Merge remote-tracking branch 'origin/master' into FR_quotient2

eric-wieser committed 3 years ago
refactor

astrainfinita committed 3 years ago
feat(data/list/pi): new file

astrainfinita committed 3 years ago
golf

astrainfinita committed 3 years ago
fix copyright

astrainfinita committed 3 years ago
Merge branch 'FR_list_pi' into FR_quotient2

astrainfinita committed 3 years ago
docs

astrainfinita committed 3 years ago
Merge branch 'FR_quotient2' into FR_dfinsupp_sigma_uncurry

astrainfinita committed 3 years ago
Update basic.lean

astrainfinita committed 3 years ago

mathlib3 feat(data/dfinsupp/basic): remove decidable typeclass assumptions on `sigma_uncurry` #18318 Open

mathlib3
feat(data/dfinsupp/basic): remove decidable typeclass assumptions on `sigma_uncurry`
#18318

Open