Documentation

Mathlib.Data.Nat.Cast.NeZero

Lemmas about nonzero elements of an AddMonoidWithOne #

theorem NeZero.one_le {n : } [NeZero n] :
1 n
theorem NeZero.natCast_ne (n : ) (R : Type u_1) [AddMonoidWithOne R] [h : NeZero n] :
n 0
theorem NeZero.of_neZero_natCast (R : Type u_1) [AddMonoidWithOne R] {n : } [h : NeZero n] :
theorem NeZero.pos_of_neZero_natCast (R : Type u_1) [AddMonoidWithOne R] {n : } [NeZero n] :
0 < n