English
The exponent additivity holds: selfZPow x B (n+m) = selfZPow x B n · selfZPow x B m.
Русский
Аддитивность показателя: selfZPow x B (n+m) = selfZPow x B n · selfZPow x B m.
LaTeX
$$$selfZPow(x,B,n+m) = selfZPow(x,B,n) \cdot selfZPow(x,B,m)$$$
Lean4
theorem selfZPow_mul_neg (d : ℤ) : selfZPow x B d * selfZPow x B (-d) = 1 :=
by
by_cases hd : d ≤ 0
· rw [selfZPow_of_nonpos x B hd, selfZPow_of_nonneg, ← map_pow, Int.natAbs_neg, Submonoid.pow_apply,
IsLocalization.mk'_spec, map_one]
apply nonneg_of_neg_nonpos
rwa [neg_neg]
· rw [selfZPow_of_nonneg x B (le_of_not_ge hd), selfZPow_of_nonpos, ← map_pow, Int.natAbs_neg, Submonoid.pow_apply,
IsLocalization.mk'_spec'_mk, map_one]
refine nonpos_of_neg_nonneg (le_of_lt ?_)
rwa [neg_neg, ← not_le]
