Commit 2023-11-05 20:38 cf8bb091

View on Github →

chore: cleanup zify imports in preparation of upstreaming (#8176)

Estimated changes

Modified Mathlib/Tactic/Zify.lean

modified theorem Mathlib.Tactic.Zify.nat_cast_dvd

modified theorem Mathlib.Tactic.Zify.nat_cast_eq

modified theorem Mathlib.Tactic.Zify.nat_cast_le

modified theorem Mathlib.Tactic.Zify.nat_cast_lt

modified theorem Mathlib.Tactic.Zify.nat_cast_ne

Modified test/Zify.lean