New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
chore(data/finset/image): reduce imports #17886
Conversation
@@ -405,16 +407,18 @@ end | |||
|
|||
lemma mem_range_iff_mem_finset_range_of_mod_eq [decidable_eq α] {f : ℤ → α} {a : α} {n : ℕ} | |||
(hn : 0 < n) (h : ∀ i, f (i % n) = f i) : | |||
a ∈ set.range f ↔ a ∈ (finset.range n).image (λi, f i) := | |||
suffices (∃ i, f (i % n) = a) ↔ ∃ i, i < n ∧ f ↑i = a, by simpa [h], |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Does the old proof no longer work?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Old proof needs some lemmas in data.int.order.basic
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Which ones?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
int.mod_nonneg
and int.mod_lt_of_pos
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm a little wary of this this split; those seem like pretty fundamental properties of mod
, so I would prefer not to have to effectively reprove them to prove this lemma.
Can you split this into two PRs; one that moves the imports, and one that changes edit: thanks!int.order.basic
to int.basic
?
This PR/issue depends on:
|
That doesn't really seem important. |
RFC. It's not important. Just seems like it shouldn't depend on
data.int.order.basic
.Maybe
int.mod_nonneg
andint.mod_lt_of_pos
should be moved to a more basic file?Zulip