Documentation

Init.Data.Nat.Linear

Helper definitions and theorems for constructing linear arithmetic proofs.

@[inline, reducible]
Instances For
    @[inline, reducible]
    Instances For

      When encoding polynomials. We use fixedVar for encoding numerals. The denotation of fixedVar is always 1.

      Instances For
        @[inline, reducible]
        Instances For
          Equations
          Instances For
            Equations
            Instances For
              Equations
              Instances For
                Instances For
                  Equations
                  Instances For
                    @[inline, reducible]
                    Instances For
                      Equations
                      Instances For