def RelHom.onFun {α : Type u_1} {β : Type u_2} (r : β → β → Prop) (f : α → β) : Function.onFun r f →r r

Equations

• RelHom.onFun r f = { toFun := f, map_rel' := ⋯ }

@[simp]

def RelHom.coe_onFun {α : Type u_1} {β : Type u_2} {r : β → β → Prop} (f : α → β) : ⇑(onFun r f) = f

Equations

• ⋯ = ⋯

instance IsWellFounded.onFun {α : Type u_1} {β : Type u_2} (r : β → β → Prop) (f : α → β) [wfl : IsWellFounded β r] : IsWellFounded α (Function.onFun r f)

def MonomialOrder.ofInjective.Syn {σ : Type u_2} (m : MonomialOrder σ) {σ' : Type u_3} (f : σ' → σ) : Type u_3

Equations

• MonomialOrder.ofInjective.Syn m f = (σ' →₀ ℕ)

noncomputable instance MonomialOrder.ofInjective.acm' {σ' : Type u_1} {σ : Type u_2} (m : MonomialOrder σ) (f : σ' → σ) : AddCommMonoid (Syn m f)

Equations

• MonomialOrder.ofInjective.acm' m f = inferInstanceAs (AddCommMonoid (σ' →₀ ℕ))

def MonomialOrder.ofInjective.toSyn' {σ : Type u_2} (m : MonomialOrder σ) {σ' : Type u_3} (f : σ' → σ) : (σ' →₀ ℕ) ≃+ Syn m f

Equations

• MonomialOrder.ofInjective.toSyn' m f = AddEquiv.refl (σ' →₀ ℕ)

noncomputable def MonomialOrder.ofInjective {σ : Type u_2} (m : MonomialOrder σ) {σ' : Type u_3} {f : σ' → σ} (hf : Function.Injective f) : MonomialOrder σ'

Equations

• One or more equations did not get rendered due to their size.

structure MonomialOrder.Embedding {σ' : Type u_1} (m' : MonomialOrder σ') {σ : Type u_2} (m : MonomialOrder σ) : Type (max u_1 u_2)

• toFun : σ' → σ
• toFun_injective : Function.Injective self.toFun
• monotone' : Monotone (⇑m.toSyn ∘ Finsupp.mapDomain self.toFun ∘ ⇑m'.toSyn.symm)

instance MonomialOrder.Embedding.instFunLike {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} : FunLike (m'.Embedding m) σ' σ

Equations

• MonomialOrder.Embedding.instFunLike = { coe := MonomialOrder.Embedding.toFun, coe_injective' := ⋯ }

theorem MonomialOrder.Embedding.ext {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} {e₁ e₂ : m'.Embedding m} (h : ⇑e₁ = ⇑e₂) : e₁ = e₂

theorem MonomialOrder.Embedding.ext_iff {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} {e₁ e₂ : m'.Embedding m} : e₁ = e₂ ↔ ⇑e₁ = ⇑e₂

@[simp]

theorem MonomialOrder.Embedding.toFun_eq_coe {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) : e.toFun = ⇑e

theorem MonomialOrder.Embedding.monotone {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) : Monotone (⇑m.toSyn ∘ Finsupp.mapDomain ⇑e ∘ ⇑m'.toSyn.symm)

theorem MonomialOrder.Embedding.coe_injective {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) : Function.Injective ⇑e

def MonomialOrder.Embedding.toStrictMono {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) : StrictMono (⇑m.toSyn ∘ Finsupp.mapDomain ⇑e ∘ ⇑m'.toSyn.symm)

Equations

• ⋯ = ⋯

noncomputable def MonomialOrder.Embedding.toOrderEmbedding {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) : m'.syn ↪o m.syn

Equations

• e.toOrderEmbedding = OrderEmbedding.ofStrictMono (⇑m.toSyn ∘ Finsupp.mapDomain ⇑e ∘ ⇑m'.toSyn.symm) ⋯

def MonomialOrder.Embedding.le_iff_le {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) (a b : m'.syn) : m.toSyn (Finsupp.mapDomain (⇑e) (m'.toSyn.symm a)) ≤ m.toSyn (Finsupp.mapDomain (⇑e) (m'.toSyn.symm b)) ↔ a ≤ b

Equations

• ⋯ = ⋯

def MonomialOrder.Embedding.le_iff_le' {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) (a b : σ' →₀ ℕ) : m.toSyn (Finsupp.mapDomain (⇑e) a) ≤ m.toSyn (Finsupp.mapDomain (⇑e) b) ↔ m'.toSyn a ≤ m'.toSyn b

Equations

• ⋯ = ⋯

def MonomialOrder.Embedding.lt_iff_lt {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) (a b : m'.syn) : m.toSyn (Finsupp.mapDomain (⇑e) (m'.toSyn.symm a)) < m.toSyn (Finsupp.mapDomain (⇑e) (m'.toSyn.symm b)) ↔ a < b

Equations

• ⋯ = ⋯

def MonomialOrder.Embedding.lt_iff_lt' {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) (a b : σ' →₀ ℕ) : m.toSyn (Finsupp.mapDomain (⇑e) a) < m.toSyn (Finsupp.mapDomain (⇑e) b) ↔ m'.toSyn a < m'.toSyn b

Equations

• ⋯ = ⋯

def MonomialOrder.Embedding.ofInjective {σ' : Type u_1} {σ : Type u_2} (m : MonomialOrder σ) {f : σ' → σ} (hf : Function.Injective f) : (m.ofInjective hf).Embedding m

Equations

• MonomialOrder.Embedding.ofInjective m hf = { toFun := f, toFun_injective := hf, monotone' := ⋯ }

theorem MonomialOrder.Embedding.ofInjective_coe {σ' : Type u_1} {σ : Type u_2} (m : MonomialOrder σ) {f : σ' → σ} (hf : Function.Injective f) : ⇑(ofInjective m hf) = f

theorem MonomialOrder.Embedding.degree_rename {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) {R : Type u_3} [CommSemiring R] (p : MvPolynomial σ' R) : m.degree ((MvPolynomial.rename ⇑e) p) = Finsupp.mapDomain (⇑e) (m'.degree p)

@[simp]

theorem MonomialOrder.Embedding.leadingCoeff_rename {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) {R : Type u_3} [CommSemiring R] (p : MvPolynomial σ' R) : m.leadingCoeff ((MvPolynomial.rename ⇑e) p) = m'.leadingCoeff p

theorem MonomialOrder.Embedding.leadingTerm_rename {σ' : Type u_1} {m' : MonomialOrder σ'} {σ : Type u_2} {m : MonomialOrder σ} (e : m'.Embedding m) {R : Type u_3} [CommSemiring R] (p : MvPolynomial σ' R) : m.leadingTerm ((MvPolynomial.rename ⇑e) p) = (MvPolynomial.rename ⇑e) (m'.leadingTerm p)