Commit 2024-05-08 08:43 994f298c

View on Github →

chore: Deduplicate zpow_ne_zero_of_ne_zero and zpow_ne_zero (#12734) Both lemmas are the same up to a binder swap. Also rename zpow_eq_zero to eq_zero_of_zpow_ne_zero.

Estimated changes

Modified Mathlib/Algebra/GroupWithZero/Power.lean

added theorem eq_zero_of_zpow_eq_zero

deleted theorem zpow_eq_zero

modified theorem zpow_eq_zero_iff

modified theorem zpow_ne_zero

added theorem zpow_ne_zero_iff

deleted theorem zpow_ne_zero_of_ne_zero

Modified Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean

Modified Mathlib/Analysis/Calculus/Deriv/ZPow.lean

Modified Mathlib/NumberTheory/Padics/PadicNorm.lean