Documentation

Mathlib.Algebra.Ring.Nat

The natural numbers form a semiring #

This file contains the commutative semiring instance on the natural numbers.

See note [foundational algebra order theory].

Instances #

Equations

Extra instances to short-circuit type class resolution #

These also prevent non-computable instances being used to construct these instances non-computably.

Equations
Equations