inductive Nat.Internal.SOM.Expr : Type

• num (i : Nat) : Expr
• var (v : Linear.Var) : Expr
• add (a b : Expr) : Expr
• mul (a b : Expr) : Expr

@[instance_reducible]

instance Nat.Internal.SOM.instInhabitedExpr : Inhabited Expr

@[inline]

noncomputable abbrev Nat.Internal.SOM.Expr.denote (ctx : Linear.Context) : Expr → Nat

@[reducible, inline]

abbrev Nat.Internal.SOM.Mon : Type

@[inline]

noncomputable abbrev Nat.Internal.SOM.Mon.denote (ctx : Linear.Context) : Mon → Nat

def Nat.Internal.SOM.Mon.mul (m₁ m₂ : Mon) : Mon

@[reducible, inline]

abbrev Nat.Internal.SOM.Poly : Type

@[inline]

noncomputable abbrev Nat.Internal.SOM.Poly.denote (ctx : Linear.Context) : Poly → Nat

def Nat.Internal.SOM.Poly.add (p₁ p₂ : Poly) : Poly

def Nat.Internal.SOM.Poly.insertSorted (k : Nat) (m : Mon) (p : Poly) : Poly

def Nat.Internal.SOM.Poly.mulMon (p : Poly) (k : Nat) (m : Mon) : Poly

def Nat.Internal.SOM.Poly.mul (p₁ p₂ : Poly) : Poly

def Nat.Internal.SOM.Expr.toPoly : Expr → Poly

theorem Nat.Internal.SOM.Mon.append_denote (ctx : Linear.Context) (m₁ m₂ : Mon) : denote ctx (m₁ ++ m₂) = denote ctx m₁ * denote ctx m₂

theorem Nat.Internal.SOM.Mon.mul_denote (ctx : Linear.Context) (m₁ m₂ : Mon) : denote ctx (m₁.mul m₂) = denote ctx m₁ * denote ctx m₂

theorem Nat.Internal.SOM.Poly.append_denote (ctx : Linear.Context) (p₁ p₂ : Poly) : denote ctx (p₁ ++ p₂) = denote ctx p₁ + denote ctx p₂

theorem Nat.Internal.SOM.Poly.add_denote (ctx : Linear.Context) (p₁ p₂ : Poly) : denote ctx (p₁.add p₂) = denote ctx p₁ + denote ctx p₂

theorem Nat.Internal.SOM.Poly.denote_insertSorted (ctx : Linear.Context) (k : Nat) (m : Mon) (p : Poly) : denote ctx (insertSorted k m p) = denote ctx p + k * Mon.denote ctx m

theorem Nat.Internal.SOM.Poly.mulMon_denote (ctx : Linear.Context) (p : Poly) (k : Nat) (m : Mon) : denote ctx (p.mulMon k m) = denote ctx p * k * Mon.denote ctx m

theorem Nat.Internal.SOM.Poly.mul_denote (ctx : Linear.Context) (p₁ p₂ : Poly) : denote ctx (p₁.mul p₂) = denote ctx p₁ * denote ctx p₂

theorem Nat.Internal.SOM.Expr.toPoly_denote (ctx : Linear.Context) (e : Expr) : Poly.denote ctx e.toPoly = denote ctx e

theorem Nat.Internal.SOM.Expr.eq_of_toPoly_eq (ctx : Linear.Context) (a b : Expr) (h : (a.toPoly == b.toPoly) = true) : denote ctx a = denote ctx b