basic): add `rel_covering`, main defs only
#18418

Open

feat(order/rel_iso/basic): add `rel_covering`, main defs only #18418

astrainfinita wants to merge 3 commits into master from FR_rel_covering

feat(order/rel_iso/basic): add `rel_covering`, defs only

f128d4be

astrainfinita added awaiting-review

astrainfinita added awaiting-CI

astrainfinita added t-order

astrainfinita changed the title ~~feat(order/rel_iso/basic): add `rel_covering`, defs only~~ feat(order/rel_iso/basic): add `rel_covering`, main defs only 3 years ago

fix

a226f055

astrainfinita requested a review 3 years ago

github-actions removed awaiting-CI

eric-wieser commented on 2023-02-10

eric-wieser removed awaiting-review

eric-wieser added awaiting-author

docs

4660d2e2

astrainfinita removed awaiting-author

astrainfinita added awaiting-review

kim-em removed awaiting-review

kim-em added awaiting-author

kim-em added merge-conflict

kim-em added modifies-synchronized-file

kim-em added too-late

kim-em removed review request 2 years ago

Reviewers

eric-wieser

Assignees

No one assigned

Labels

awaiting-author merge-conflict t-order modifies-synchronized-file too-late

Milestone

No milestone

mathlib3 feat(order/rel_iso/basic): add `rel_covering`, main defs only #18418 Open

feat(order/rel_iso/basic): add `rel_covering`, main defs only #18418

mathlib3
feat(order/rel_iso/basic): add `rel_covering`, main defs only
#18418

Open