Documentation

Mathlib.Tactic.Positivity.Basic

positivity core extensions #

This file sets up the basic positivity extensions tagged with the @[positivity] attribute.

The positivity extension which identifies expressions of the form ite p a b, such that positivity successfully recognises both a and b.

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

    The positivity extension which identifies expressions of the form min a b, such that positivity successfully recognises both a and b.

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

      Extension for the max operator. The max of two numbers is nonnegative if at least one is nonnegative, strictly positive if at least one is positive, and nonzero if both are nonzero.

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

        The positivity extension which identifies expressions of the form a + b, such that positivity successfully recognises both a and b.

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

          The positivity extension which identifies expressions of the form a * b, such that positivity successfully recognises both a and b.

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

            The positivity extension which identifies expressions of the form a / b, where a and b are integers.

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

              The positivity extension which identifies expressions of the form a / b, such that positivity successfully recognises both a and b.

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

                The positivity extension which identifies expressions of the form a⁻¹, such that positivity successfully recognises a.

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

                  The positivity extension which identifies expressions of the form a ^ (0:ℕ). This extension is run in addition to the general a ^ b extension (they are overlapping).

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

                    The positivity extension which identifies expressions of the form a ^ (0:ℤ).

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

                      The positivity extension which identifies expressions of the form a ^ (b : ℕ), such that positivity successfully recognises both a and b.

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

                        The positivity extension which identifies expressions of the form |a|.

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

                          Extension for the positivity tactic: Int.natAbs is positive when its input is. Since the output type of Int.natAbs is , the nonnegative case is handled by the default positivity tactic.

                          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

                                Extension for Nat.succ.

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

                                  Extension for Nat.factorial.

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