Documentation

Init.Grind.Module.NatModuleNorm

source
def Lean.Grind.Linarith.Expr.denoteN {α : Type u_1} [NatModule α] (ctx : Context α) :
Expr → α
Equations
Instances For
    source
    inductive Lean.Grind.Linarith.Poly.NonnegCoeffs :
    Poly → Prop
    Instances For
      source
      def Lean.Grind.Linarith.Poly.denoteN {α : Type u_1} [NatModule α] (ctx : Context α) (p : Poly) :
      α
      Equations
      Instances For
        source
        theorem Lean.Grind.Linarith.Poly.denoteN_nil {α : Type u_1} [NatModule α] (ctx : Context α) :
        denoteN ctx nil = 0
        source
        theorem Lean.Grind.Linarith.Poly.denoteN_add {α : Type u_1} [NatModule α] (ctx : Context α) (k : Int) (x : Var) (p : Poly) :
        k ≥ 0 → denoteN ctx (add k x p) = k.toNat • Var.denote ctx x + denoteN ctx p
        source
        theorem Lean.Grind.Linarith.instAssociativeHAdd_1 {α : Type u_1} [NatModule α] :
        Std.Associative fun (x1 x2 : α) => x1 + x2
        source
        theorem Lean.Grind.Linarith.instCommutativeHAdd_1 {α : Type u_1} [NatModule α] :
        Std.Commutative fun (x1 x2 : α) => x1 + x2
        source
        theorem Lean.Grind.Linarith.Poly.denoteN_insert {α : Type u_1} [NatModule α] (ctx : Context α) (k : Int) (x : Var) (p : Poly) :
        k ≥ 0 → p.NonnegCoeffs → denoteN ctx (insert k x p) = k.toNat • Var.denote ctx x + denoteN ctx p
        source
        theorem Lean.Grind.Linarith.Poly.denoteN_append {α : Type u_1} [NatModule α] (ctx : Context α) (p₁ p₂ : Poly) :
        p₁.NonnegCoeffs → p₂.NonnegCoeffs → denoteN ctx (p₁.append p₂) = denoteN ctx p₁ + denoteN ctx p₂
        source
        theorem Lean.Grind.Linarith.Poly.denoteN_combine {α : Type u_1} [NatModule α] (ctx : Context α) (p₁ p₂ : Poly) :
        p₁.NonnegCoeffs → p₂.NonnegCoeffs → denoteN ctx (p₁.combine p₂) = denoteN ctx p₁ + denoteN ctx p₂
        source
        theorem Lean.Grind.Linarith.Poly.denoteN_mul' {α : Type u_1} [NatModule α] (ctx : Context α) (p : Poly) (k : Nat) :
        p.NonnegCoeffs → denoteN ctx (p.mul' ↑k) = k • denoteN ctx p
        source
        theorem Lean.Grind.Linarith.Poly.denoteN_mul {α : Type u_1} [NatModule α] (ctx : Context α) (p : Poly) (k : Nat) :
        p.NonnegCoeffs → denoteN ctx (p.mul ↑k) = k • denoteN ctx p
        source
        def Lean.Grind.Linarith.Expr.toPolyN :
        Expr → Poly
        Equations
        Instances For
          source
          theorem Lean.Grind.Linarith.Poly.mul'_Nonneg (p : Poly) (k : Nat) :
          p.NonnegCoeffs → (p.mul' ↑k).NonnegCoeffs
          source
          theorem Lean.Grind.Linarith.Poly.mul_Nonneg (p : Poly) (k : Nat) :
          p.NonnegCoeffs → (p.mul ↑k).NonnegCoeffs
          source
          theorem Lean.Grind.Linarith.Poly.append_Nonneg (p₁ p₂ : Poly) :
          p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.append p₂).NonnegCoeffs
          source
          theorem Lean.Grind.Linarith.Poly.combine_Nonneg (p₁ p₂ : Poly) :
          p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.combine p₂).NonnegCoeffs
          source
          theorem Lean.Grind.Linarith.Expr.toPolyN_Nonneg (e : Expr) :
          e.toPolyN.NonnegCoeffs
          source
          theorem Lean.Grind.Linarith.Expr.denoteN_toPolyN {α : Type u_1} [NatModule α] (ctx : Context α) (e : Expr) :
          Poly.denoteN ctx e.toPolyN = denoteN ctx e
          source
          def Lean.Grind.Linarith.eq_normN_cert (lhs rhs : Expr) :
          Bool
          Equations
          Instances For
            source
            theorem Lean.Grind.Linarith.eq_normN {α : Type u_1} [NatModule α] (ctx : Context α) (lhs rhs : Expr) :
            eq_normN_cert lhs rhs = true → Expr.denoteN ctx lhs = Expr.denoteN ctx rhs