Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 11cdc8c

Browse files
committed
feat(data/polynomial/*) : as_sum_support (#4286)
1 parent 0ccc157 commit 11cdc8c

File tree

4 files changed

+17
-6
lines changed

4 files changed

+17
-6
lines changed

src/data/polynomial/algebra_map.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -80,7 +80,7 @@ section comp
8080

8181
lemma eval₂_comp [comm_semiring S] (f : R →+* S) {x : S} :
8282
(p.comp q).eval₂ f x = p.eval₂ f (q.eval₂ f x) :=
83-
by rw [comp, p.as_sum]; simp only [eval₂_mul, eval₂_C, eval₂_pow, eval₂_finset_sum, eval₂_X]
83+
by rw [comp, p.as_sum_range]; simp only [eval₂_mul, eval₂_C, eval₂_pow, eval₂_finset_sum, eval₂_X]
8484

8585

8686
lemma eval_comp : (p.comp q).eval a = p.eval (q.eval a) := eval₂_comp _

src/data/polynomial/degree/basic.lean

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -194,14 +194,24 @@ begin
194194
{ exact (coeff_eq_zero_of_nat_degree_lt (not_le.1 (λ w, h (nat.lt_one_add_iff.2 w)))).symm, }
195195
end
196196

197-
lemma as_sum (p : polynomial R) :
197+
lemma as_sum_range (p : polynomial R) :
198198
p = ∑ i in range (p.nat_degree + 1), C (p.coeff i) * X^i :=
199199
begin
200200
ext n,
201201
simp only [add_comm, coeff_X_pow, coeff_C_mul, finset.mem_range,
202202
finset.sum_mul_boole, finset_sum_coeff, ite_le_nat_degree_coeff],
203203
end
204204

205+
lemma as_sum_support (p : polynomial R) :
206+
p = ∑ i in p.support, C (p.coeff i) * X^i :=
207+
begin
208+
ext n,
209+
simp only [finset_sum_coeff, coeff_C_mul, coeff_X_pow, finset.sum_mul_boole],
210+
split_ifs,
211+
{ refl },
212+
{ contrapose h, rw not_not, exact mem_support_iff_coeff_ne_zero.mpr h }
213+
end
214+
205215
/--
206216
We can reexpress a sum over `p.support` as a sum over `range n`,
207217
for any `n` satisfying `p.nat_degree < n`.

src/data/polynomial/eval.lean

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -181,7 +181,7 @@ lemma eval₂_pow (n : ℕ) : (p ^ n).eval₂ f x = p.eval₂ f x ^ n := (eval
181181

182182
lemma eval₂_eq_sum_range :
183183
p.eval₂ f x = ∑ i in finset.range (p.nat_degree + 1), f (p.coeff i) * x^i :=
184-
trans (congr_arg _ p.as_sum) (trans (eval₂_finset_sum f _ _ x) (congr_arg _ (by simp)))
184+
trans (congr_arg _ p.as_sum_range) (trans (eval₂_finset_sum f _ _ x) (congr_arg _ (by simp)))
185185

186186
end eval₂
187187

@@ -222,7 +222,8 @@ lemma eval_sum (p : polynomial R) (f : ℕ → R → polynomial R) (x : R) :
222222
(p.sum f).eval x = p.sum (λ n a, (f n a).eval x) :=
223223
eval₂_sum _ _ _ _
224224

225-
225+
lemma eval_finset_sum (s : finset ι) (g : ι → polynomial R) (x : R) :
226+
(∑ i in s, g i).eval x = ∑ i in s, (g i).eval x := eval₂_finset_sum _ _ _ _
226227

227228
/-- `is_root p x` implies `x` is a root of `p`. The evaluation of `p` at `x` is zero -/
228229
def is_root (p : polynomial R) (a : R) : Prop := p.eval a = 0
@@ -395,7 +396,7 @@ lemma mem_map_range {p : polynomial S} :
395396
begin
396397
split,
397398
{ rintro ⟨p, rfl⟩ n, rw coeff_map, exact set.mem_range_self _ },
398-
{ intro h, rw p.as_sum,
399+
{ intro h, rw p.as_sum_range,
399400
apply is_add_submonoid.finset_sum_mem,
400401
intros i hi,
401402
rcases h i with ⟨c, hc⟩,

src/data/polynomial/monic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ variables [semiring R] {p q r : polynomial R}
3030
lemma monic.as_sum {p : polynomial R} (hp : p.monic) :
3131
p = X^(p.nat_degree) + (∑ i in finset.range p.nat_degree, C (p.coeff i) * X^i) :=
3232
begin
33-
conv_lhs { rw [p.as_sum, finset.sum_range_succ] },
33+
conv_lhs { rw [p.as_sum_range, finset.sum_range_succ] },
3434
suffices : C (p.coeff p.nat_degree) = 1,
3535
{ rw [this, one_mul] },
3636
exact congr_arg C hp

0 commit comments

Comments
 (0)