Theorem NeZero.one_le
Modification history
2025-12-04 09:22
Mathlib/Data/Nat/Cast/NeZero.lean
feat(Tactic): add `lia` as an alias for `cutsat` and use it throughout (#32376) …
Modified NeZero.one_leView on Github →2025-09-24 05:32
Mathlib/Data/Nat/Cast/NeZero.lean
chore: replace omega with cutsat where possible (#29461) …
Modified NeZero.one_leView on Github →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 →