Skip to content

Commit

Permalink
refactor(data/polynomial): use monic.ne_zero and nontriviality (#…
Browse files Browse the repository at this point in the history 
…9530)

There is a pattern in `data/polynomial` to have both `(hq : q.monic) (hq0 : q ≠ 0)` as assumptions. I found this less convenient to work with than `[nontrivial R] (hq : q.monic)` and using `monic.ne_zero` to replace `hq0`.

The `nontriviality` tactic automates all the cases where previously `nontrivial R` (or similar) was manually derived from the hypotheses.
  • Loading branch information
@Vierkantor
Vierkantor committed Oct 5, 2021
1 parent fd18953 commit 1536412
Show file tree
Hide file tree
Showing 5 changed files with 83 additions and 100 deletions.
164 changes: 75 additions & 89 deletions src/data/polynomial/div.lean
View file
Expand Up @@ -106,14 +106,14 @@ infixl ` /ₘ ` : 70 := div_by_monic

infixl ` %ₘ ` : 70 := mod_by_monic

lemma degree_mod_by_monic_lt : ∀ (p : polynomial R) {q : polynomial R} (hq : monic q)
(hq0 : q ≠ 0), degree (p %ₘ q) < degree q
| p := λ q hq hq0,
lemma degree_mod_by_monic_lt [nontrivial R] : ∀ (p : polynomial R) {q : polynomial R}
(hq : monic q), degree (p %ₘ q) < degree q
| p := λ q hq,
if h : degree q ≤ degree p ∧ p ≠ 0 then
have wf : _ := div_wf_lemma ⟨h.1, h.2⟩ hq,
have degree ((p - C (leading_coeff p) * X ^ (nat_degree p - nat_degree q) * q) %ₘ q) < degree q :=
degree_mod_by_monic_lt (p - C (leading_coeff p) * X ^ (nat_degree p - nat_degree q) * q)
hq hq0,
hq,
begin
unfold mod_by_monic at this ⊢,
unfold div_mod_by_monic_aux,
Expand All @@ -132,7 +132,7 @@ else
unfold mod_by_monic div_mod_by_monic_aux,
rw [dif_pos hq, if_neg h, not_not.1 hp],
exact lt_of_le_of_ne bot_le
(ne.symm (mt degree_eq_bot.1 hq0)),
(ne.symm (mt degree_eq_bot.1 hq.ne_zero)),
end
using_well_founded {dec_tac := tactic.assumption}

Expand Down Expand Up @@ -164,23 +164,17 @@ lemma div_by_monic_eq_of_not_monic (p : polynomial R) (hq : ¬monic q) : p /ₘ

lemma mod_by_monic_eq_of_not_monic (p : polynomial R) (hq : ¬monic q) : p %ₘ q = p := dif_neg hq

lemma mod_by_monic_eq_self_iff (hq : monic q) (hq0 : q ≠ 0) : p %ₘ q = p ↔ degree p < degree q :=
⟨λ h, h ▸ degree_mod_by_monic_lt _ hq hq0,
lemma mod_by_monic_eq_self_iff [nontrivial R] (hq : monic q) : p %ₘ q = p ↔ degree p < degree q :=
⟨λ h, h ▸ degree_mod_by_monic_lt _ hq,
λ h, have ¬ degree q ≤ degree p := not_le_of_gt h,
by unfold mod_by_monic div_mod_by_monic_aux; rw [dif_pos hq, if_neg (mt and.left this)]⟩

theorem degree_mod_by_monic_le (p : polynomial R) {q : polynomial R}
(hq : monic q) : degree (p %ₘ q) ≤ degree q :=
decidable.by_cases
(assume H : q = 0, by rw [monic, H, leading_coeff_zero] at hq;
have : (0:polynomial R) = 1 := (by rw [← C_0, ← C_1, hq]);
exact le_of_eq (congr_arg _ $ eq_of_zero_eq_one this (p %ₘ q) q))
(assume H : q ≠ 0, le_of_lt $ degree_mod_by_monic_lt _ hq H)
by { nontriviality R, exact (degree_mod_by_monic_lt _ hq).le }

end ring



section comm_ring
variables [comm_ring R] {p q : polynomial R}

Expand Down Expand Up @@ -209,38 +203,36 @@ using_well_founded {dec_tac := tactic.assumption}
lemma mod_by_monic_add_div (p : polynomial R) {q : polynomial R} (hq : monic q) :
p %ₘ q + q * (p /ₘ q) = p := eq_sub_iff_add_eq.1 (mod_by_monic_eq_sub_mul_div p hq)

lemma div_by_monic_eq_zero_iff (hq : monic q) (hq0 : q ≠ 0) : p /ₘ q = 0 ↔ degree p < degree q :=
lemma div_by_monic_eq_zero_iff [nontrivial R] (hq : monic q) : p /ₘ q = 0 ↔ degree p < degree q :=
⟨λ h, by have := mod_by_monic_add_div p hq;
rwa [h, mul_zero, add_zero, mod_by_monic_eq_self_iff hq hq0] at this,
rwa [h, mul_zero, add_zero, mod_by_monic_eq_self_iff hq] at this,
λ h, have ¬ degree q ≤ degree p := not_le_of_gt h,
by unfold div_by_monic div_mod_by_monic_aux; rw [dif_pos hq, if_neg (mt and.left this)]⟩

lemma degree_add_div_by_monic (hq : monic q) (h : degree q ≤ degree p) :
degree q + degree (p /ₘ q) = degree p :=
if hq0 : q = 0 then
have ∀ (p : polynomial R), p = 0,
from λ p, (@subsingleton_of_monic_zero R _ (hq0 ▸ hq)).1 _ _,
by rw [this (p /ₘ q), this p, this q]; refl
else
have hdiv0 : p /ₘ q ≠ 0 := by rwa [(≠), div_by_monic_eq_zero_iff hq hq0, not_lt],
have hlc : leading_coeff q * leading_coeff (p /ₘ q) ≠ 0 :=
by rwa [monic.def.1 hq, one_mul, (≠), leading_coeff_eq_zero],
have hmod : degree (p %ₘ q) < degree (q * (p /ₘ q)) :=
calc degree (p %ₘ q) < degree q : degree_mod_by_monic_lt _ hq hq0
... ≤ _ : by rw [degree_mul' hlc, degree_eq_nat_degree hq0,
degree_eq_nat_degree hdiv0, ← with_bot.coe_add, with_bot.coe_le_coe];
exact nat.le_add_right _ _,
calc degree q + degree (p /ₘ q) = degree (q * (p /ₘ q)) : eq.symm (degree_mul' hlc)
... = degree (p %ₘ q + q * (p /ₘ q)) : (degree_add_eq_right_of_degree_lt hmod).symm
... = _ : congr_arg _ (mod_by_monic_add_div _ hq)
begin
nontriviality R,
have hdiv0 : p /ₘ q ≠ 0 := by rwa [(≠), div_by_monic_eq_zero_iff hq, not_lt],
have hlc : leading_coeff q * leading_coeff (p /ₘ q) ≠ 0 :=
by rwa [monic.def.1 hq, one_mul, (≠), leading_coeff_eq_zero],
have hmod : degree (p %ₘ q) < degree (q * (p /ₘ q)) :=
calc degree (p %ₘ q) < degree q : degree_mod_by_monic_lt _ hq
... ≤ _ : by rw [degree_mul' hlc, degree_eq_nat_degree hq.ne_zero,
degree_eq_nat_degree hdiv0, ← with_bot.coe_add, with_bot.coe_le_coe];
exact nat.le_add_right _ _,
calc degree q + degree (p /ₘ q) = degree (q * (p /ₘ q)) : eq.symm (degree_mul' hlc)
... = degree (p %ₘ q + q * (p /ₘ q)) : (degree_add_eq_right_of_degree_lt hmod).symm
... = _ : congr_arg _ (mod_by_monic_add_div _ hq)
end

lemma degree_div_by_monic_le (p q : polynomial R) : degree (p /ₘ q) ≤ degree p :=
if hp0 : p = 0 then by simp only [hp0, zero_div_by_monic, le_refl]
else if hq : monic q then
have hq0 : q ≠ 0 := hq.ne_zero_of_polynomial_ne hp0,
if h : degree q ≤ degree p
then by rw [← degree_add_div_by_monic hq h, degree_eq_nat_degree hq0,
degree_eq_nat_degree (mt (div_by_monic_eq_zero_iff hq hq0).1 (not_lt.2 h))];
then by haveI := nontrivial.of_polynomial_ne hp0;
rw [← degree_add_div_by_monic hq h, degree_eq_nat_degree hq.ne_zero,
degree_eq_nat_degree (mt (div_by_monic_eq_zero_iff hq).1 (not_lt.2 h))];
exact with_bot.coe_le_coe.2 (nat.le_add_left _ _)
else
by unfold div_by_monic div_mod_by_monic_aux;
Expand All @@ -249,17 +241,18 @@ else (div_by_monic_eq_of_not_monic p hq).symm ▸ bot_le

lemma degree_div_by_monic_lt (p : polynomial R) {q : polynomial R} (hq : monic q)
(hp0 : p ≠ 0) (h0q : 0 < degree q) : degree (p /ₘ q) < degree p :=
have hq0 : q ≠ 0 := hq.ne_zero_of_polynomial_ne hp0,
if hpq : degree p < degree q
then begin
rw [(div_by_monic_eq_zero_iff hq hq0).2 hpq, degree_eq_nat_degree hp0],
haveI := nontrivial.of_polynomial_ne hp0,
rw [(div_by_monic_eq_zero_iff hq).2 hpq, degree_eq_nat_degree hp0],
exact with_bot.bot_lt_coe _
end
else begin
rw [← degree_add_div_by_monic hq (not_lt.1 hpq), degree_eq_nat_degree hq0,
degree_eq_nat_degree (mt (div_by_monic_eq_zero_iff hq hq0).1 hpq)],
haveI := nontrivial.of_polynomial_ne hp0,
rw [← degree_add_div_by_monic hq (not_lt.1 hpq), degree_eq_nat_degree hq.ne_zero,
degree_eq_nat_degree (mt (div_by_monic_eq_zero_iff hq).1 hpq)],
exact with_bot.coe_lt_coe.2 (nat.lt_add_of_pos_left
(with_bot.coe_lt_coe.1 $ (degree_eq_nat_degree hq0) ▸ h0q))
(with_bot.coe_lt_coe.1 $ (degree_eq_nat_degree hq.ne_zero) ▸ h0q))
end

theorem nat_degree_div_by_monic {R : Type u} [comm_ring R] (f : polynomial R) {g : polynomial R}
Expand All @@ -271,9 +264,9 @@ begin
nat_degree_zero] },
haveI : nontrivial R := ⟨⟨0, 1, h01⟩⟩,
by_cases hfg : f /ₘ g = 0,
{ rw [hfg, nat_degree_zero], rw div_by_monic_eq_zero_iff hg hg.ne_zero at hfg,
{ rw [hfg, nat_degree_zero], rw div_by_monic_eq_zero_iff hg at hfg,
rw nat.sub_eq_zero_of_le (nat_degree_le_nat_degree $ le_of_lt hfg) },
have hgf := hfg, rw div_by_monic_eq_zero_iff hg hg.ne_zero at hgf, push_neg at hgf,
have hgf := hfg, rw div_by_monic_eq_zero_iff hg at hgf, push_neg at hgf,
have := degree_add_div_by_monic hg hgf,
have hf : f ≠ 0, { intro hf, apply hfg, rw [hf, zero_div_by_monic] },
rw [degree_eq_nat_degree hf, degree_eq_nat_degree hg.ne_zero, degree_eq_nat_degree hfg,
Expand All @@ -283,9 +276,8 @@ end

lemma div_mod_by_monic_unique {f g} (q r : polynomial R) (hg : monic g)
(h : r + g * q = f ∧ degree r < degree g) : f /ₘ g = q ∧ f %ₘ g = r :=
if hg0 : g = 0 then by split; exact (subsingleton_of_monic_zero
(hg0 ▸ hg : monic (0 : polynomial R))).1 _ _
else
begin
nontriviality R,
have h₁ : r - f %ₘ g = -g * (q - f /ₘ g),
from eq_of_sub_eq_zero
(by rw [← sub_eq_zero_of_eq (h.1.trans (mod_by_monic_add_div f hg).symm)];
Expand All @@ -295,35 +287,34 @@ else
have h₄ : degree (r - f %ₘ g) < degree g,
from calc degree (r - f %ₘ g) ≤ max (degree r) (degree (f %ₘ g)) :
degree_sub_le _ _
... < degree g : max_lt_iff.2 ⟨h.2, degree_mod_by_monic_lt _ hg hg0⟩,
... < degree g : max_lt_iff.2 ⟨h.2, degree_mod_by_monic_lt _ hg⟩,
have h₅ : q - (f /ₘ g) = 0,
from by_contradiction
(λ hqf, not_le_of_gt h₄ $
calc degree g ≤ degree g + degree (q - f /ₘ g) :
by erw [degree_eq_nat_degree hg0, degree_eq_nat_degree hqf,
by erw [degree_eq_nat_degree hg.ne_zero, degree_eq_nat_degree hqf,
with_bot.coe_le_coe];
exact nat.le_add_right _ _
... = degree (r - f %ₘ g) :
by rw [h₂, degree_mul']; simpa [monic.def.1 hg]),
⟨eq.symm $ eq_of_sub_eq_zero h₅,
exact ⟨eq.symm $ eq_of_sub_eq_zero h₅,
eq.symm $ eq_of_sub_eq_zero $ by simpa [h₅] using h₁⟩
end

lemma map_mod_div_by_monic [comm_ring S] (f : R →+* S) (hq : monic q) :
(p /ₘ q).map f = p.map f /ₘ q.map f ∧ (p %ₘ q).map f = p.map f %ₘ q.map f :=
if h01 : (0 : S) = 1 then by haveI := subsingleton_of_zero_eq_one h01;
exact ⟨subsingleton.elim _ _, subsingleton.elim _ _⟩
else
have h01R : (0 : R) ≠ 1, from mt (congr_arg f)
(by rwa [f.map_one, f.map_zero]),
have map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q),
from (div_mod_by_monic_unique ((p /ₘ q).map f) _ (monic_map f hq)
⟨eq.symm $ by rw [← map_mul, ← map_add, mod_by_monic_add_div _ hq],
calc _ ≤ degree (p %ₘ q) : degree_map_le _ _
... < degree q : degree_mod_by_monic_lt _ hq
$ (hq.ne_zero_of_ne h01R)
... = _ : eq.symm $ degree_map_eq_of_leading_coeff_ne_zero _
(by rw [monic.def.1 hq, f.map_one]; exact ne.symm h01)⟩),
⟨this.1.symm, this.2.symm⟩
begin
nontriviality S,
haveI : nontrivial R := f.domain_nontrivial,
have : map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q),
{ exact (div_mod_by_monic_unique ((p /ₘ q).map f) _ (monic_map f hq)
⟨eq.symm $ by rw [← map_mul, ← map_add, mod_by_monic_add_div _ hq],
calc _ ≤ degree (p %ₘ q) : degree_map_le _ _
... < degree q : degree_mod_by_monic_lt _ hq
... = _ : eq.symm $ degree_map_eq_of_leading_coeff_ne_zero _
(by rw [monic.def.1 hq, f.map_one]; exact one_ne_zero)⟩) },
exact ⟨this.1.symm, this.2.symm⟩
end

lemma map_div_by_monic [comm_ring S] (f : R →+* S) (hq : monic q) :
(p /ₘ q).map f = p.map f /ₘ q.map f :=
Expand All @@ -336,23 +327,23 @@ lemma map_mod_by_monic [comm_ring S] (f : R →+* S) (hq : monic q) :
lemma dvd_iff_mod_by_monic_eq_zero (hq : monic q) : p %ₘ q = 0 ↔ q ∣ p :=
⟨λ h, by rw [← mod_by_monic_add_div p hq, h, zero_add];
exact dvd_mul_right _ _,
λ h, if hq0 : q = 0 then by rw hq0 at hq;
exact (subsingleton_of_monic_zero hq).1 _ _
else
let ⟨r, hr⟩ := exists_eq_mul_right_of_dvd h in
by_contradiction (λ hpq0,
have hmod : p %ₘ q = q * (r - p /ₘ q) :=
by rw [mod_by_monic_eq_sub_mul_div _ hq, mul_sub, ← hr],
have degree (q * (r - p /ₘ q)) < degree q :=
hmod ▸ degree_mod_by_monic_lt _ hq hq0,
λ h, begin
nontriviality R,
obtain ⟨r, hr⟩ := exists_eq_mul_right_of_dvd h,
by_contradiction hpq0,
have hmod : p %ₘ q = q * (r - p /ₘ q),
{ rw [mod_by_monic_eq_sub_mul_div _ hq, mul_sub, ← hr] },
have : degree (q * (r - p /ₘ q)) < degree q :=
hmod ▸ degree_mod_by_monic_lt _ hq,
have hrpq0 : leading_coeff (r - p /ₘ q) ≠ 0 :=
λ h, hpq0 $ leading_coeff_eq_zero.1
(by rw [hmod, leading_coeff_eq_zero.1 h, mul_zero, leading_coeff_zero]),
have hlc : leading_coeff q * leading_coeff (r - p /ₘ q) ≠ 0 :=
by rwa [monic.def.1 hq, one_mul],
by rw [degree_mul' hlc, degree_eq_nat_degree hq0,
degree_eq_nat_degree (mt leading_coeff_eq_zero.2 hrpq0)] at this;
exact not_lt_of_ge (nat.le_add_right _ _) (with_bot.some_lt_some.1 this))⟩
rw [degree_mul' hlc, degree_eq_nat_degree hq.ne_zero,
degree_eq_nat_degree (mt leading_coeff_eq_zero.2 hrpq0)] at this,
exact not_lt_of_ge (nat.le_add_right _ _) (with_bot.some_lt_some.1 this)
end⟩

theorem map_dvd_map [comm_ring S] (f : R →+* S) (hf : function.injective f) {x y : polynomial R}
(hx : x.monic) : x.map f ∣ y.map f ↔ x ∣ y :=
Expand All @@ -371,22 +362,17 @@ by conv_rhs { rw [← mod_by_monic_add_div p monic_one] }; simp

@[simp] lemma mod_by_monic_X_sub_C_eq_C_eval (p : polynomial R) (a : R) :
p %ₘ (X - C a) = C (p.eval a) :=
if h0 : (0 : R) = 1 then by letI := subsingleton_of_zero_eq_one h0; exact subsingleton.elim _ _
else
by haveI : nontrivial R := nontrivial_of_ne 0 1 h0; exact
have h : (p %ₘ (X - C a)).eval a = p.eval a :=
by rw [mod_by_monic_eq_sub_mul_div _ (monic_X_sub_C a), eval_sub, eval_mul,
eval_sub, eval_X, eval_C, sub_self, zero_mul, sub_zero],
have degree (p %ₘ (X - C a)) < 1 :=
degree_X_sub_C a ▸ degree_mod_by_monic_lt p (monic_X_sub_C a) ((degree_X_sub_C a).symm ▸
ne_zero_of_monic (monic_X_sub_C _)),
have degree (p %ₘ (X - C a)) ≤ 0 :=
begin
cases (degree (p %ₘ (X - C a))),
{ exact bot_le },
{ exact with_bot.some_le_some.2 (nat.le_of_lt_succ (with_bot.some_lt_some.1 this)) }
end,
begin
nontriviality R,
have h : (p %ₘ (X - C a)).eval a = p.eval a,
{ rw [mod_by_monic_eq_sub_mul_div _ (monic_X_sub_C a), eval_sub, eval_mul,
eval_sub, eval_X, eval_C, sub_self, zero_mul, sub_zero] },
have : degree (p %ₘ (X - C a)) < 1 :=
degree_X_sub_C a ▸ degree_mod_by_monic_lt p (monic_X_sub_C a),
have : degree (p %ₘ (X - C a)) ≤ 0,
{ cases (degree (p %ₘ (X - C a))),
{ exact bot_le },
{ exact with_bot.some_le_some.2 (nat.le_of_lt_succ (with_bot.some_lt_some.1 this)) } },
rw [eq_C_of_degree_le_zero this, eval_C] at h,
rw [eq_C_of_degree_le_zero this, h]
end
Expand Down
4 changes: 1 addition & 3 deletions src/data/polynomial/field_division.lean
View file
Expand Up @@ -121,8 +121,6 @@ private lemma remainder_lt_aux (p : polynomial R) (hq : q ≠ 0) :
degree (mod p q) < degree q :=
by rw ← degree_mul_leading_coeff_inv q hq; exact
degree_mod_by_monic_lt p (monic_mul_leading_coeff_inv hq)
(mul_ne_zero hq (mt leading_coeff_eq_zero.2 (by rw leading_coeff_C;
exact inv_ne_zero (mt leading_coeff_eq_zero.1 hq))))

instance : has_div (polynomial R) := ⟨div⟩

Expand Down Expand Up @@ -173,7 +171,7 @@ lemma div_eq_zero_iff (hq0 : q ≠ 0) : p / q = 0 ↔ degree p < degree q :=
λ h, have hlt : degree p < degree (q * C (leading_coeff q)⁻¹),
by rwa degree_mul_leading_coeff_inv q hq0,
have hm : monic (q * C (leading_coeff q)⁻¹) := monic_mul_leading_coeff_inv hq0,
by rw [div_def, (div_by_monic_eq_zero_iff hm (ne_zero_of_monic hm)).2 hlt, mul_zero]⟩
by rw [div_def, (div_by_monic_eq_zero_iff hm).2 hlt, mul_zero]⟩

lemma degree_add_div (hq0 : q ≠ 0) (hpq : degree q ≤ degree p) :
degree q + degree (p / q) = degree p :=
Expand Down
8 changes: 4 additions & 4 deletions src/data/polynomial/ring_division.lean
View file
Expand Up @@ -253,8 +253,8 @@ then
rw degree_eq_nat_degree hp at hpd,
exact with_bot.coe_le_coe.2 (with_bot.coe_lt_coe.1 hpd)
end,
have hdiv0 : p /ₘ (X - C x) ≠ 0 := mt (div_by_monic_eq_zero_iff (monic_X_sub_C x)
(ne_zero_of_monic (monic_X_sub_C x))).1 $ not_lt.2 hdeg,
have hdiv0 : p /ₘ (X - C x) ≠ 0 := mt (div_by_monic_eq_zero_iff (monic_X_sub_C x)).1 $
not_lt.2 hdeg,
⟨x ::ₘ t, calc (card (x ::ₘ t) : with_bot ℕ) = t.card + 1 :
by exact_mod_cast card_cons _ _
... ≤ degree p :
Expand Down Expand Up @@ -577,10 +577,10 @@ begin
have hp := mod_by_monic_add_div p hmonic,
have hzero : (p /ₘ q) ≠ 0,
{ intro h,
exact not_lt_of_le hdegree ((div_by_monic_eq_zero_iff hmonic (monic.ne_zero hmonic)).1 h) },
exact not_lt_of_le hdegree ((div_by_monic_eq_zero_iff hmonic).1 h) },
have deglt : (p %ₘ q).degree < (q * (p /ₘ q)).degree,
{ rw degree_mul,
refine lt_of_lt_of_le (degree_mod_by_monic_lt p hmonic (monic.ne_zero hmonic)) _,
refine lt_of_lt_of_le (degree_mod_by_monic_lt p hmonic) _,
rw [degree_eq_nat_degree (monic.ne_zero hmonic), degree_eq_nat_degree hzero],
norm_cast,
simp only [zero_le, le_add_iff_nonneg_right] },
Expand Down
2 changes: 1 addition & 1 deletion src/field_theory/minpoly.lean
View file
Expand Up @@ -289,7 +289,7 @@ begin
by_contra hnz,
have := degree_le_of_ne_zero A x hnz _,
{ contrapose! this,
exact degree_mod_by_monic_lt _ (monic hx) (ne_zero hx) },
exact degree_mod_by_monic_lt _ (monic hx) },
{ rw ← mod_by_monic_add_div p (monic hx) at hp,
simpa using hp }
end
Expand Down
5 changes: 2 additions & 3 deletions src/ring_theory/power_basis.lean
View file
Expand Up @@ -251,8 +251,7 @@ begin
have : (f %ₘ minpoly A pb.gen).nat_degree < pb.dim,
{ rw ← pb.nat_degree_minpoly,
apply nat_degree_lt_nat_degree hf,
exact degree_mod_by_monic_lt _ (minpoly.monic pb.is_integral_gen)
(minpoly.ne_zero pb.is_integral_gen) },
exact degree_mod_by_monic_lt _ (minpoly.monic pb.is_integral_gen) },
rw [aeval_eq_sum_range' this, aeval_eq_sum_range' this, linear_map.map_sum],
refine finset.sum_congr rfl (λ i (hi : i ∈ finset.range pb.dim), _),
rw finset.mem_range at hi,
Expand Down Expand Up @@ -435,7 +434,7 @@ begin
apply mem_span_pow'.mpr _,
have := minpoly.monic hx,
refine ⟨f.mod_by_monic (minpoly R x),
lt_of_lt_of_le (degree_mod_by_monic_lt _ this (ne_zero_of_monic this)) degree_le_nat_degree,
lt_of_lt_of_le (degree_mod_by_monic_lt _ this) degree_le_nat_degree,
_⟩,
conv_lhs { rw ← mod_by_monic_add_div f this },
simp only [add_zero, zero_mul, minpoly.aeval, aeval_add, alg_hom.map_mul]
Expand Down

0 comments on commit 1536412

Please sign in to comment.