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
@[reducible, inline]
abbrev Lean.Grind.CommRing.Expr.toPolyM (e : Meta.Grind.Arith.CommRing.RingExpr) :
Meta.Grind.Arith.CommRing.RingM Poly

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

Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Lean.Grind.CommRing.Poly.mulConstM (p : Poly) (k : Int) :
      Meta.Grind.Arith.CommRing.RingM Poly
      Equations
        Instances For
          source
          @[reducible, inline]
          abbrev Lean.Grind.CommRing.Poly.mulMonM (p : Poly) (k : Int) (m : Mon) :
          Meta.Grind.Arith.CommRing.RingM Poly
          Equations
            Instances For
              source
              @[reducible, inline]
              abbrev Lean.Grind.CommRing.Poly.mulM (p₁ p₂ : Poly) :
              Meta.Grind.Arith.CommRing.RingM Poly
              Equations
                Instances For
                  source
                  @[reducible, inline]
                  abbrev Lean.Grind.CommRing.Poly.combineM (p₁ p₂ : Poly) :
                  Meta.Grind.Arith.CommRing.RingM Poly
                  Equations
                    Instances For
                      source
                      def Lean.Grind.CommRing.Poly.spolM (p₁ p₂ : Poly) :
                      Meta.Grind.Arith.CommRing.RingM SPolResult
                      Equations
                        Instances For