[Merged by Bors] - refactor(data/polynomial): Move some lemmas to monoid_algebra

[eric-wieser]

The add_monoid_algebra.mul_apply_antidiagonal lemma is copied verbatim from monoid_algebra.mul_apply_antidiagonal.

---

[eric-wieser]

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?

[urkud]

mul_single_apply_aux is used more than 1 time in monoid_algebra.

[eric-wieser]

Good point.

[urkud]

I left a couple of comments. LGTM otherwise.
bors d+

[bors]

✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[eric-wieser]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests