[Merged by Bors] - feat: The support of f ^ n#9617
[Merged by Bors] - feat: The support of f ^ n#9617YaelDillies wants to merge 19 commits intomasterfrom
f ^ n#9617Conversation
This involves moving lemmas from `Algebra.GroupPower.Ring` to `Algebra.GroupWithZero.Basic` and changing some `0 < n` assumptions to `n ≠ 0`. From LeanAPAP
d83d587 to
1cfda43
Compare
j-loreaux
left a comment
There was a problem hiding this comment.
Overall very nice thanks! Only some minor comments.
bors d+
|
|
||
| theorem pow_pos_iff (hn : 0 < n) : 0 < a ^ n ↔ 0 < a := by | ||
| simp_rw [zero_lt_iff, pow_ne_zero_iff hn] | ||
| theorem pow_pos_iff (hn : n ≠ 0) : 0 < a ^ n ↔ 0 < a := by simp_rw [zero_lt_iff, pow_ne_zero_iff hn] |
There was a problem hiding this comment.
This is very minor, and I'm not asking you to change it now, but in the future it would be nice if these kinds of changes were avoided because they needlessly increase the diff, and, as far as style is concerned, the community guidelines are ambivalent on this issue.
There was a problem hiding this comment.
It doesn't increase the diff here given that those lines were already modified.
| rw [eq_div_iff hzero, ← sub_eq_zero] at h | ||
| replace hzero : s ≠ 0 := by rintro rfl; simp only [map_zero, not_true_eq_false] at hzero | ||
| let f : F[X] := X ^ m * expand F n s - expand F n r | ||
| refine ⟨f, ?_, ?_⟩ | ||
| · have : f.coeff (n * s.natDegree + m) ≠ 0 := by | ||
| have hn : 0 < n := by linarith only [hm, hmn] | ||
| have hndvd : ¬ n ∣ n * s.natDegree + m := by | ||
| rw [← Nat.dvd_add_iff_right (n.dvd_mul_right s.natDegree)] | ||
| exact Nat.not_dvd_of_pos_of_lt hm hmn | ||
| simp only [coeff_sub, coeff_X_pow_mul, s.coeff_expand_mul' hn, coeff_natDegree, | ||
| coeff_expand hn r, hndvd, ite_false, sub_zero] | ||
| exact leadingCoeff_ne_zero.2 hzero | ||
| intro h | ||
| simp only [h, coeff_zero, ne_eq, not_true_eq_false] at this | ||
| · simp only [map_sub, map_mul, map_pow, aeval_X, expand_aeval, h] |
There was a problem hiding this comment.
the same comment applies here, except in this case I think the style guidelines do recommend the · with indentation here (i.e., how it was before the edit), so please revert to shrink the diff.
There was a problem hiding this comment.
No, the style guide says · can (and probably should) be removed when one branch is much longer than the other ones.
| apply Finset.sum_congr rfl | ||
| refine' fun m _ => mul_eq_mul_left_iff.mpr (Or.inl _) | ||
| rw [ite_pow, zero_pow (pow_pos hp.out.pos _)] | ||
| rw [ite_pow, zero_pow (pow_ne_zero _ hp.out.ne_zero)] |
There was a problem hiding this comment.
This idiom was repeated a few times in the diff, but I think this is slightly nicer (untested):
| rw [ite_pow, zero_pow (pow_ne_zero _ hp.out.ne_zero)] | |
| rw [ite_pow, zero_pow (pow_pos hp.out.pos _).ne'] |
It's possible I'm missing something though.
There was a problem hiding this comment.
I understand the idea, but I'm not sure this is better. The "correct" proof of course is
| rw [ite_pow, zero_pow (pow_ne_zero _ hp.out.ne_zero)] | |
| rw [ite_pow, zero_pow (by positivity)] |
but I haven't made it work yet (nor am I sure I can make it work without a performance penalty, actually). I am happy to wait for this to be figured out before merging this PR if you think that's important.
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
|
Build failed (retrying...): |
|
Build failed: |
|
bors merge |
|
Pull request successfully merged into master. Build succeeded: |
f ^ nf ^ n
This involves moving lemmas from
Algebra.GroupPower.RingtoAlgebra.GroupWithZero.Basicand changing some0 < nassumptions ton ≠ 0.From LeanAPAP