Mathlib v3 is deprecated. Go to Mathlib v4

Theorem zpow_neg_coe_of_pos

Modification history

2022-01-12 00:08
src/algebra/group_power/basic.lean
feat(analysis/special_functions/pow): norm_num extension for rpow (#11382) …
Added zpow_neg_coe_of_posView on Github →