-
Notifications
You must be signed in to change notification settings - Fork 297
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
[Merged by Bors] - refactor(data/polynomial): Move some lemmas to monoid_algebra
#4627
Conversation
The `add_monoid_algebra.mul_apply_antidiagonal` lemma is copied verbatim from `monoid_algebra.mul_apply_antidiagonal`.
The docstring for `coeff_single` says it shouldn't be needed and `coeff_monomial` is the preferred spelling
@[simp] lemma coeff_mul_C (p : polynomial R) (n : ℕ) (a : R) : | ||
coeff (p * C a) n = coeff p n * a := | ||
begin | ||
conv_rhs { rw [← @finsupp.sum_single _ _ _ p, coeff_sum] }, | ||
rw [add_monoid_algebra.mul_def, ←monomial_zero_left], simp_rw [sum_single_index], | ||
{ simp only [coeff_single, finsupp.sum_mul, coeff_sum], | ||
apply sum_congr rfl, | ||
assume i hi, by_cases i = n; simp [h], }, | ||
end | ||
add_monoid_algebra.mul_single_zero_apply p a n |
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.
Note that this proof is actually longer in add_monoid_algebra
:
mathlib/src/algebra/monoid_algebra.lean
Lines 598 to 612 in 7559d1c
lemma mul_single_apply_aux (f : add_monoid_algebra k G) (r : k) | |
(x y z : G) (H : ∀ a, a + x = z ↔ a = y) : | |
(f * single x r) z = f y * r := | |
have A : ∀ a₁ b₁, (single x r).sum (λ a₂ b₂, ite (a₁ + a₂ = z) (b₁ * b₂) 0) = | |
ite (a₁ + x = z) (b₁ * r) 0, | |
from λ a₁ b₁, sum_single_index $ by simp, | |
calc (f * single x r) z = sum f (λ a b, if (a = y) then (b * r) else 0) : | |
-- different `decidable` instances make it not trivial | |
by { simp only [mul_apply, A, H], congr, funext, split_ifs; refl } | |
... = if y ∈ f.support then f y * r else 0 : f.support.sum_ite_eq' _ _ | |
... = f y * r : by split_ifs with h; simp at h; simp [h] | |
lemma mul_single_zero_apply (f : add_monoid_algebra k G) (r : k) (x : G) : | |
(f * single 0 r) x = f x * r := | |
f.mul_single_apply_aux r _ _ _ $ λ a, by rw [add_zero] |
Should I change the proof there to use this shorter proof, or is the long one more readable?
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.
mul_single_apply_aux
is used more than 1 time in monoid_algebra
.
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.
Good point.
This allows the lemma which "ideally wouldn't be necessary" to not be necessary
0fdb368
to
75646cd
Compare
I left a couple of comments. LGTM otherwise. |
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
The `add_monoid_algebra.mul_apply_antidiagonal` lemma is copied verbatim from `monoid_algebra.mul_apply_antidiagonal`.
Pull request successfully merged into master. Build succeeded: |
monoid_algebra
monoid_algebra
The
add_monoid_algebra.mul_apply_antidiagonal
lemma is copied verbatim frommonoid_algebra.mul_apply_antidiagonal
.