Nonzero integers

Content created by Fredrik Bakke, Egbert Rijke and malarbol.

Created on 2023-10-06.
Last modified on 2024-04-11.

module elementary-number-theory.nonzero-integers where
open import elementary-number-theory.integers
open import elementary-number-theory.natural-numbers

open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.negation
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels


An integer k is said to be nonzero if the proposition

  k ≠ 0



The predicate of being a nonzero integer

is-nonzero-prop-ℤ :   Prop lzero
is-nonzero-prop-ℤ k = neg-type-Prop (k  zero-ℤ)

is-nonzero-ℤ :   UU lzero
is-nonzero-ℤ k = type-Prop (is-nonzero-prop-ℤ k)

is-prop-is-nonzero-ℤ : (k : )  is-prop (is-nonzero-ℤ k)
is-prop-is-nonzero-ℤ k = is-prop-type-Prop (is-nonzero-prop-ℤ k)

The nonzero integers

nonzero-ℤ : UU lzero
nonzero-ℤ = type-subtype is-nonzero-prop-ℤ

module _
  (k : nonzero-ℤ)

  int-nonzero-ℤ : 
  int-nonzero-ℤ = pr1 k

  is-nonzero-nonzero-ℤ : is-nonzero-ℤ int-nonzero-ℤ
  is-nonzero-nonzero-ℤ = pr2 k

The nonzero integer 1

is-nonzero-one-ℤ : is-nonzero-ℤ one-ℤ
is-nonzero-one-ℤ ()

one-nonzero-ℤ : nonzero-ℤ
pr1 one-nonzero-ℤ = one-ℤ
pr2 one-nonzero-ℤ = is-nonzero-one-ℤ


The integer image of a nonzero natural number is nonzero

is-nonzero-int-ℕ : (n : )  is-nonzero-ℕ n  is-nonzero-ℤ (int-ℕ n)
is-nonzero-int-ℕ zero-ℕ H p = H refl

The negative of a nonzero integer is nonzero

is-nonzero-neg-nonzero-ℤ : (x : )  is-nonzero-ℤ x  is-nonzero-ℤ (neg-ℤ x)
is-nonzero-neg-nonzero-ℤ x H K = H (is-zero-is-zero-neg-ℤ x K)

Recent changes