Theorem NeZero.pos_of_neZero_natCast

Modification history

2023-09-05 09:13
Mathlib/Data/Nat/Cast/Defs.lean
chore: separate NeZero dependency from Nat/Cast/Defs (#6955) …
Modified NeZero.pos_of_neZero_natCastView on Github →
2022-11-20 00:17
Mathlib/Data/Nat/Cast/Defs.lean
feat: port data.{nat, int}.cast.defs (#641) …
Added NeZero.pos_of_neZero_natCastView on Github →