equivNonZeroDivisorsNat — Mathlib

English

The positive natural numbers ℕ⁺ are order-monoid equivalent to the nonZeroDivisors of ℕ; i.e., there is an order-monoid isomorphism between ℕ⁺ and nonZeroDivisors(ℕ).

Русский

Положительные натуральные числа ℕ⁺ эквивалентны по порядку и умножению множеству nonZeroDivisors(ℕ); существует упорядоченно-монойдное изоморфизм между ℕ⁺ и nonZeroDivisors(ℕ).

LaTeX

$$ℕ^{+} \; \cong_*o\; nonZeroDivisors(\mathbb{N})$$

Lean4

/-- `ℕ+` is equivalent to `nonZeroDivisors ℕ` in terms of order and multiplication. -/
@[simps]
def equivNonZeroDivisorsNat : ℕ+ ≃*o nonZeroDivisors ℕ
    where
  toFun x := ⟨x.val, by simp⟩
  invFun x := ⟨x.val, by simp [Nat.pos_iff_ne_zero]⟩
  map_mul' := by simp
  map_le_map_iff' := by simp

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