feat(ring_theory/mv_polynomial/symmetric): sum of symmetric polynomials is symmetric

[Xialu3421]

---

Hi, this is my first PR. Thanks!

[eric-wieser]

I think you can prove this in one line with something like

(symmetric_subalgebra σ R).sum_mem _

[Xialu3421]

Thank you! I will edit it.

________________________________ From: Eric Wieser ***@***.***> Sent: 24 March 2023 05:07 To: leanprover-community/mathlib ***@***.***> Cc: Zheng, Xialu ***@***.***>; Author ***@***.***> Subject: Re: [leanprover-community/mathlib] feat(ring_theory/mv_polynomial/symmetric): sum of symmetric polynomials is symmetric (PR #18640) This email from ***@***.*** originates from outside Imperial. Do not click on links and attachments unless you recognise the sender. If you trust the sender, add them to your safe senders list<https://spam.ic.ac.uk/SpamConsole/Senders.aspx> to disable email stamping for this address. @eric-wieser commented on this pull request.

________________________________ In src/ring_theory/mv_polynomial/symmetric.lean<#18640 (comment)>:

@@ -109,6 +109,18 @@ lemma mul (hφ : is_symmetric φ) (hψ : is_symmetric ψ) : is_symmetric (φ *

lemma smul (r : R) (hφ : is_symmetric φ) : is_symmetric (r • φ) := (symmetric_subalgebra σ R).smul_mem hφ r +lemma sum {α : Type*} [decidable_eq α] {s : finset α} {f : α → mv_polynomial σ R} : + (∀ a ∈ s, (f a).is_symmetric) → (∑ a in s, f a).is_symmetric := +begin I think you can prove this in one line with something like (symmetric_subalgebra σ R).sum_mem _ — Reply to this email directly, view it on GitHub<#18640 (review)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AZ5BQX6NDGOPACKCWFSMTWLW5S3Q5ANCNFSM6AAAAAAWFVQKEQ>. You are receiving this because you authored the thread.Message ID: ***@***.***>