isUnit_iff — Mathlib

English

Let n be a natural number. Then n is a unit in the multiplicative monoid (N, ×) if and only if n = 1.

Русский

Пусть n ∈ ℕ. Тогда n является единицей в моноиде умножения (ℕ, ×) тогда и только тогда, когда n = 1.

LaTeX

$$$ \forall n \in \mathbb{N}, \; \mathrm{IsUnit}(n) \iff n = 1 $$$

Lean4

/-- Alias of `isUnit_iff_eq_one` for discoverability. -/
protected theorem isUnit_iff {n : ℕ} : IsUnit n ↔ n = 1 :=
  isUnit_iff_eq_one

Похожие утверждения