Documentation

Mathlib.Data.Nat.Cast.NeZero

Lemmas about nonzero elements of an AddMonoidWithOne #

source
theorem NeZero.natCast_ne (n : ℕ) (R : Type u_1) [AddMonoidWithOne R] [h : NeZero ↑n] :
↑n ≠ 0
source
theorem NeZero.of_neZero_natCast (R : Type u_1) [AddMonoidWithOne R] {n : ℕ} [h : NeZero ↑n] :
NeZero n
source
theorem NeZero.pos_of_neZero_natCast (R : Type u_1) [AddMonoidWithOne R] {n : ℕ} [NeZero ↑n] :
0 < n