mathlib3
feat(order/well_founded): `well_founded_lt.has_min`, etc.
#18751

Open

feat(order/well_founded): `well_founded_lt.has_min`, etc. #18751

vihdzp wants to merge 6 commits into master from wf_has_min

cleanup

3ba74c2e

Update well_founded.lean

e2095cee

these are all automatically inferred

07c4504d

add better has_min

1dc2f42f

Merge branch 'wf_cleanup_1' into wf_has_min

be1b026d

vihdzp added awaiting-review

mathlib-dependent-issues-bot added blocked-by-other-PR

break symmetry

88b2a9ad

vihdzp marked this pull request as draft 2 years ago

kim-em added too-late

Reviewers

No reviews

Assignees

No one assigned

Labels

awaiting-review blocked-by-other-PR too-late

Milestone

No milestone