Documentation

Mathlib.Algebra.Order.Monoid.PNat

Equivalence between ℕ+ and nonZeroDivisors ℕ #

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

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

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