## Stream: maths

### Topic: mv_polynomial puzzles

#### Kevin Buzzard (Jan 25 2020 at 13:01):

I keep coming up with these. Do we have this one? What is it called, if so?

import data.mv_polynomial

open mv_polynomial

example {R : Type*} [comm_semiring R] {σ : Type*} {p : mv_polynomial σ R} :
finset.sum p.support (λ s, monomial s (p.coeff s)) = p := sorry


#### Kevin Buzzard (Jan 25 2020 at 13:29):

I am such a hacker:

example {R : Type*} [comm_semiring R] {σ : Type*} {p : mv_polynomial σ R} :
finset.sum p.support (λ s, monomial s (p.coeff s)) = p :=
begin
apply mv_polynomial.ext,
intro s,
rw coeff_sum,
simp only [coeff_monomial],
by_cases hs : s ∈ p.support,
{ rw ←finset.sum_subset (show {s} ⊆ p.support, begin
intros i hi,
convert hs,
cases hi, assumption, cases hi
end),
swap,
{ intros t ht hts,
rw if_neg,
intro hts2,
apply hts,
rw hts2,
apply set.mem_singleton,
},
convert finset.sum_singleton,
rw if_pos,
refl
},
{ rw ←finset.sum_subset (finset.empty_subset p.support),
swap,
{ intros t ht1 ht2,
rw if_neg,
intro hts,
apply hs,
rwa hts at ht1,
},
rw finset.sum_empty,
rw finsupp.mem_support_iff at hs,
symmetry,
apply classical.not_not.1 hs
}
end


I sometimes feel like I write Lean the way a child would.

Last updated: May 18 2021 at 06:15 UTC