# 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 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.

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.

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.

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.

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.

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.

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.

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.

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

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

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.

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

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

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.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.

Extension for Nat.succ.

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