mathlib3
refactor(order/rel_classes): remove redundant hypothesis from `is_well_order`
#18702
Open
Overview
Commits
2
Changes
View On GitHub

refactor(order/rel_classes): remove redundant hypothesis from `is_well_order` #18702

vihdzp wants to merge 2 commits into master from is_well_order_weaken
vihdzp
vihdzp remove redundant hypothesis
9a296d33
vihdzp vihdzp added awaiting-review
vihdzp vihdzp added awaiting-CI
vihdzp vihdzp added modifies-synchronized-file
vihdzp vihdzp changed the title refactor: remove redundant hypothesis from `is_well_order` refactor(order/rel_classes): remove redundant hypothesis from `is_well_order` 2 years ago
github-actions github-actions removed awaiting-CI
eric-wieser
eric-wieser commented on 2023-03-31
eric-wieser eric-wieser requested a review from YaelDillies YaelDillies 2 years ago
eric-wieser eric-wieser added t-order
vihdzp added doc comments
d62da6c9
eric-wieser eric-wieser added not-too-late

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
awaiting-review t-order modifies-synchronized-file not-too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum