Structures · Data types

Nat.AtLeastTwo

A type class for natural numbers which are greater than or equal to 2. NeZero and AtLeastTwo are used for numeric literals, and also for groups of related lemmas sharing a common value of n that needs to be nonzero, or at least 2, and where it is convenient to pass this information implicitly. Instances for these classes cover some of the cases where it is most structurally obvious from the syntactic form of n that it satisfies the required conditions, such as m + 1. Less widely used cases may be defined as lemmas rather than global instances and then made into instances locally where needed. If implicit arguments, appearing before other explicit arguments, are allowed to be autoParams in a future version of Lean, such an autoParam that is proved by lia might be a more general replacement for the use of typeclass inference for this purpose.

Defined in

Mathlib.Data.Nat.Init

Shape

One type argument · adds prop