Documentation

Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly

The polynomial functions at Poly.lean are used for constructing proofs-by-reflection, but they do not provide mechanisms for aborting expensive computations.

source
@[inline]
def Lean.Grind.CommRing.Expr.toPolyM? (e : Meta.Grind.Arith.CommRing.RingExpr) :
Meta.Grind.Arith.CommRing.RingM (Option Poly)

Converts the given ring expression into a multivariate polynomial. If the ring has a nonzero characteristic, it is used during normalization.

Instances For
    source
    @[inline]
    def Lean.Grind.CommRing.Poly.mulConstM (p : Poly) (k : Int) :
    Meta.Grind.Arith.CommRing.RingM Poly
    Instances For
      source
      @[inline]
      def Lean.Grind.CommRing.Poly.mulMonM (p : Poly) (k : Int) (m : Mon) :
      Meta.Grind.Arith.CommRing.RingM Poly
      Instances For
        source
        @[inline]
        def Lean.Grind.CommRing.Poly.mulM (p₁ p₂ : Poly) :
        Meta.Grind.Arith.CommRing.RingM Poly
        Instances For
          source
          @[inline]
          def Lean.Grind.CommRing.Poly.combineM (p₁ p₂ : Poly) :
          Meta.Grind.Arith.CommRing.RingM Poly
          Instances For
            source
            def Lean.Grind.CommRing.Poly.spolM (p₁ p₂ : Poly) :
            Meta.Grind.Arith.CommRing.RingM SPolResult
            Instances For
              source
              def Lean.Grind.CommRing.Mon.findInvNumeralVar? (m : Mon) :
              Meta.Grind.Arith.CommRing.RingM (Option (Nat × Var))

              Returns some (val, x) if m contains a variable x whose the denotation is val⁻¹.

              Instances For
                source
                def Lean.Grind.CommRing.Poly.findInvNumeralVar? (p : Poly) :
                Meta.Grind.Arith.CommRing.RingM (Option (Nat × Var))

                Returns some (val, x) if p contains a variable x whose the denotation is val⁻¹.

                Instances For
                  source
                  structure Lean.Meta.Grind.Arith.CommRing.SimpResult :
                  Type

                  Result of simplifying a polynomial p₁ using a polynomial p₂.

                  The simplification rewrites the first monomial of p₁ that can be divided by the leading monomial of p₂.

                  • p : Poly

                    The resulting simplified polynomial after rewriting.

                  • k₁ : Int

                    The integer coefficient multiplied with polynomial p₁ in the rewriting step.

                  • k₂ : Int

                    The integer coefficient multiplied with polynomial p₂ during rewriting.

                  • m₂ : Mon

                    The monomial factor applied to polynomial p₂.

                  Instances For
                    source
                    def Lean.Grind.CommRing.Poly.simpM? (p₁ p₂ : Poly) :
                    Meta.Grind.Arith.CommRing.RingM (Option Meta.Grind.Arith.CommRing.SimpResult)

                    Simplifies polynomial p₁ using polynomial p₂ by rewriting.

                    This function attempts to rewrite p₁ by eliminating the first occurrence of the leading monomial of p₂.

                    Instances For