Commit 2026-04-27 14:17 5aa3ca30

View on Github →

chore(Tactic/Zify): remove lemmas (#38361)

Estimated changes

Modified Mathlib/Tactic/Zify.lean

deleted theorem Mathlib.Tactic.Zify.natCast_dvd

deleted theorem Mathlib.Tactic.Zify.natCast_eq

deleted theorem Mathlib.Tactic.Zify.natCast_le

deleted theorem Mathlib.Tactic.Zify.natCast_lt