mathlib3
feat(data/dfinsupp/basic): remove decidable typeclass assumptions on `sigma_uncurry`
#18318
Open
Open
feat(data/dfinsupp/basic): remove decidable typeclass assumptions on `sigma_uncurry` #18318
astrainfinita
wants to merge
26 commits into
master
from
FR_dfinsupp_sigma_uncurry
feat:(data/*/quot): quotient_lift on a finite family
3afb37b4
fix
c8c94a7f
fix
83c651cc
lint & docs
d2ad947f
`Sort`
9023f174
feat(data/quot): make `trunc` a quotient
717e6fd1
Merge branch 'FR_trunc' into FR_dfinsupp_sigma_uncurry
dc4e0620
feat(data/dfinsupp/basic): remove some typeclass assumptions on `sigm…
13d41c10
fix
b006d2e1
docs
234a4976
Merge branch 'FR_trunc' into FR_dfinsupp_sigma_uncurry
48a6e40d
astrainfinita
changed the title
docs
454cd397
golf
59b6bb18
tweak names
47c7ba23
fix
d3fc21f1
golf
5b4f3f3a
use fintype version quotient_lift
7f407d12
Merge remote-tracking branch 'origin/master' into FR_quotient2
84c0c2aa
refactor
8da5a83b
feat(data/list/pi): new file
62ed6b58
golf
7a4901c1
fix copyright
92e3d9d2
Merge branch 'FR_list_pi' into FR_quotient2
4b411b28
docs
350eb252
Merge branch 'FR_quotient2' into FR_dfinsupp_sigma_uncurry
3b8ae4ca
Update basic.lean
46e271be
Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-review
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub