finite): prove lemmas to handle part_enat.card
#19198

Closed

[Merged by Bors] - feat(set_theory/cardinal/finite): prove lemmas to handle part_enat.card #19198

AntoineChambert-Loir wants to merge 11 commits into master from acl_partenat

function to handle oart_enat.card

9fbe34bd

Merge branch 'master' into acl_partenat

612ee951

github-actions added modifies-synchronized-file

AntoineChambert-Loir added awaiting-review

to avoid 100 char limit

dff05aae

AntoineChambert-Loir changed the title ~~feat: prove lemmas to handle part_enat.card~~ feat(set_theory/cardinal): prove lemmas to handle part_enat.card 2 years ago

AntoineChambert-Loir changed the title ~~feat(set_theory/cardinal): prove lemmas to handle part_enat.card~~ feat(set_theory/cardinal/finite): prove lemmas to handle part_enat.card 2 years ago

remove #lint comment

3defaaef

remove #lint

c6e7c256

urkud commented on 2023-06-21

urkud removed awaiting-review

urkud added awaiting-author

modifs urkud + floris

b38e0ccc

more modifications

d5bccfb1

modifs complete

b2152795

linter complains

ec22cfc3

other complaints

26de341b

one application was not renamed

4c8e1a1d

AntoineChambert-Loir removed awaiting-author

AntoineChambert-Loir added awaiting-review

AntoineChambert-Loir requested a review from

fpvandoorn 2 years ago

github-actions added ready-to-merge

github-actions removed awaiting-review

bors changed the title ~~feat(set_theory/cardinal/finite): prove lemmas to handle part_enat.card~~ [Merged by Bors] - feat(set_theory/cardinal/finite): prove lemmas to handle part_enat.card 2 years ago

bors closed this 2 years ago

bors deleted the acl_partenat branch 2 years ago

Reviewers

urkud

fpvandoorn

Assignees

No one assigned

Labels

ready-to-merge modifies-synchronized-file

Milestone

No milestone

mathlib3 [Merged by Bors] - feat(set_theory/cardinal/finite): prove lemmas to handle part_enat.card #19198 Closed

[Merged by Bors] - feat(set_theory/cardinal/finite): prove lemmas to handle part_enat.card #19198

mathlib3
[Merged by Bors] - feat(set_theory/cardinal/finite): prove lemmas to handle part_enat.card
#19198

Closed