Commit 2024-11-20 11:42 333a8fa7

View on Github →

feat: Nat.cast_nonpos (#19247) For simp confluence From GrowthInGroups

Estimated changes

Modified Mathlib/Data/Int/Defs.lean

modified theorem Int.natCast_nonpos_iff

Modified Mathlib/Data/Nat/Cast/Order/Basic.lean

added theorem Nat.cast_nonpos