Mathlib.Data.Nat.Cast.NeZero

NeZero.one_le theorem

{n : ℕ} [NeZero n] : 1 ≤ n

Full source

theorem one_le {n : ℕ} [NeZero n] : 1 ≤ n := by have := NeZero.ne n; omega

Nonzero Natural Numbers Are At Least One

Informal description

For any natural number $n$ that is known to be nonzero (i.e., $n \neq 0$), we have $1 \leq n$.

NeZero.natCast_ne theorem

(n : ℕ) (R) [AddMonoidWithOne R] [h : NeZero (n : R)] : (n : R) ≠ 0

Full source

lemma natCast_ne (n : ℕ) (R) [AddMonoidWithOne R] [h : NeZero (n : R)] : (n : R) ≠ 0 := h.out

Nonzero natural number cast remains nonzero in additive monoid with one

Informal description

For any natural number $n$ and any additive monoid with one $R$, if the image of $n$ in $R$ is nonzero (i.e., $n : R \neq 0$), then $n$ itself is nonzero in $R$.

NeZero.of_neZero_natCast theorem

(R) [AddMonoidWithOne R] {n : ℕ} [h : NeZero (n : R)] : NeZero n

Full source

lemma of_neZero_natCast (R) [AddMonoidWithOne R] {n : ℕ} [h : NeZero (n : R)] : NeZero n :=
  ⟨by rintro rfl; exact h.out Nat.cast_zero⟩

Nonzero natural number cast implies nonzero original

Informal description

Let $R$ be an additive monoid with one, and let $n$ be a natural number such that the image of $n$ in $R$ is nonzero. Then $n$ is itself nonzero.

NeZero.pos_of_neZero_natCast theorem

(R) [AddMonoidWithOne R] {n : ℕ} [NeZero (n : R)] : 0 < n

Full source

lemma pos_of_neZero_natCast (R) [AddMonoidWithOne R] {n : ℕ} [NeZero (n : R)] : 0 < n :=
  Nat.pos_of_ne_zero (of_neZero_natCast R).out

Positivity of Natural Number with Nonzero Cast in Additive Monoid with One

Informal description

Let $R$ be an additive monoid with one, and let $n$ be a natural number such that the image of $n$ in $R$ is nonzero. Then $n$ is positive, i.e., $0 < n$.