Nat.isUnit_iff

theorem Nat.isUnit_iff : ∀ {n : ℕ}, IsUnit n ↔ n = 1

This theorem states that for any natural number `n`, `n` is a unit in the monoid of natural numbers under multiplication if and only if `n` is equal to 1. In other words, in the context of natural numbers, the only unit, i.e., the only number that has a multiplicative inverse, is 1.

More concisely: The natural number `n` is a multiplicative unit in the monoid of natural numbers if and only if `n` equals 1.