Documentation

Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr

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

    Given an equation c₁ containing the monomial a*x, and a divisibility constraint c₂ containing the monomial b*x, eliminate x by applying substitution.

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

      Asserts divisibility constraint.

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