Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-10-30 20:45
bdf38cf5
View on Github →
chore(*): rename int_pow to zpow (
#10058
) Leftovers of
#9989
Estimated changes
Modified
src/algebra/group_with_zero/power.lean
Modified
src/algebra/order/archimedean.lean
deleted
theorem
exists_int_pow_near'
deleted
theorem
exists_int_pow_near
added
theorem
exists_zpow_near'
added
theorem
exists_zpow_near
Modified
src/analysis/normed_space/basic.lean
Modified
src/linear_algebra/matrix/zpow.lean
Modified
src/set_theory/surreal/dyadic.lean
deleted
theorem
surreal.nsmul_int_pow_two_pow_half
added
theorem
surreal.zsmul_pow_two_pow_half