Documentation

Mathlib.Algebra.Order.Monoid.PNat

Equivalence between ℕ+ and nonZeroDivisors ℕ #

source
🔸 coverage
def PNat.equivNonZeroDivisorsNat :
ℕ+ ≃*o ↥(nonZeroDivisors ℕ)

ℕ+ is equivalent to nonZeroDivisors ℕ in terms of order and multiplication.

Equations
    Instances For
      source
      📐 coverage
      @[simp]
      theorem PNat.equivNonZeroDivisorsNat_apply_coe (x : ℕ+) :
      ↑(equivNonZeroDivisorsNat x) = ↑x
      source
      📐 coverage
      @[simp]
      theorem PNat.equivNonZeroDivisorsNat_symm_apply_coe (x : ↥(nonZeroDivisors ℕ)) :
      ↑(equivNonZeroDivisorsNat.symm x) = ↑x