Theorem NeZero.one_le

Modification history

2024-07-03 02:04
Mathlib/Algebra/Order/Group/Nat.lean
chore (Data.Nat.Cast.Order): split into `Basic` and `Ring` (#14371) …
Modified NeZero.one_leView on Github →
2024-04-07 07:06
Mathlib/Algebra/Order/Group/Nat.lean
chore: Split `Data.{Nat,Int}{.Order}.Basic` in group vs ring instances (#11924) …
Modified NeZero.one_leView on Github →
2024-03-26 23:09
Mathlib/Data/Nat/Order/Basic.lean
chore(Data/Nat): Use Std lemmas (#11661) …
Modified NeZero.one_leView on Github →
2024-02-26 00:38
Mathlib/Data/Nat/Order/Basic.lean
chore: add lemmas for nat literals corresponding to lemmas for nat casts (#8006) …
Added NeZero.one_leView on Github →