Weak Division #

Reference #

instance Pi.irrefl_lex {ι : Type u_3} {β : ι → Type u_4} (r : ι → ι → Prop) (s : {i : ι} → β i → β i → Prop) [∀ (i : ι), Std.Irrefl s] :

theorem Finset.apply_piecewise_congr {α : Type u_4} {π : α → Type u_3} {f g : (i : α) → π i} (s t : Finset α) (a : α) [(a : α) → Decidable (a ∈ s)] [(a : α) → Decidable (a ∈ t)] (ha : a ∈ s ↔ a ∈ t) :

theorem Finset.Colex.lt_iff {α : Type u_3} [LinearOrder α] (l₁ l₂ : Colex (Finset α)) :

l₁ < l₂ ↔ ∃ (a : α), (∀ b > a, b ∈ ofColex l₁ ↔ b ∈ ofColex l₂) ∧ a ∈ ofColex l₂ ∧ a ∉ ofColex l₁

theorem Finset.Colex.lt_iff_pi_lex_lt_pi_lex {α : Type u_4} {π : α → Type u_3} [LinearOrder α] [(a : α) → PartialOrder (π a)] (f g : (a : α) → π a) (h : ∀ (a : α), f a > g a) (l₁ l₂ : Colex (Finset α)) :

l₁ < l₂ ↔ Pi.Lex (fun (x1 x2 : α) => x1 > x2) (fun {i : α} (x1 x2 : π i) => x1 < x2) ((ofColex l₁).piecewise f g) ((ofColex l₂).piecewise f g)

theorem Finset.Colex.strictMono_toColex_piecewise_ofColex {α : Type u_4} {π : α → Type u_3} [LinearOrder α] [(a : α) → PartialOrder (π a)] (f g : (a : α) → π a) (h : ∀ (a : α), f a > g a) :

a ∉ f.support

theorem MonomialOrder.weakDiv {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [CommRing R] {ι : Type u_3} {b : ι → MvPolynomial σ R} (f : MvPolynomial σ R) :

∃ (g : ι →₀ MvPolynomial σ R) (r : MvPolynomial σ R), f = (Finsupp.linearCombination (MvPolynomial σ R) b) g + r ∧ (∀ (i : ι), m.toWithBotSyn (m.withBotDegree (b i) + m.withBotDegree (g i)) ≤ m.toWithBotSyn (m.withBotDegree f)) ∧ ∀ e ∈ r.support, ∀ (c : ι →₀ R), (∀ i ∈ c.support, m.degree (b i) ≤ e) → r.coeff e ≠ (Finsupp.linearCombination R (m.leadingCoeff ∘ b)) c

∃ (g : ↑B →₀ MvPolynomial σ R) (r : MvPolynomial σ R), f = (Finsupp.linearCombination (MvPolynomial σ R) fun (b : ↑B) => ↑b) g + r ∧ (∀ (b : ↑B), m.toWithBotSyn (m.withBotDegree ↑b + m.withBotDegree (g b)) ≤ m.toWithBotSyn (m.withBotDegree f)) ∧ ∀ e ∈ r.support, ∀ (c : ↑B →₀ R), (∀ b ∈ c.support, m.degree ↑b ≤ e) → r.coeff e ≠ (Finsupp.linearCombination R (m.leadingCoeff ∘ Subtype.val)) c