English
The selfZPow at m − n corresponds to a product of selfZPow m and a suitable localization mk' with a removal.
Русский
SelfZPow на m − n соответствует произведению selfZPow m на подходящую локализацию mk'.
LaTeX
$$$selfZPow(x,B,m-n) = selfZPow(x,B,m) \cdot mk'(B, a, 1)$$$
Lean4
@[simp]
theorem selfZPow_sub_natCast {n m : ℕ} : selfZPow x B (n - m) = mk' _ (x ^ n) (Submonoid.pow x m) :=
by
by_cases h : m ≤ n
·
rw [IsLocalization.eq_mk'_iff_mul_eq, Submonoid.pow_apply, Subtype.coe_mk, ← Int.ofNat_sub h, selfZPow_natCast, ←
map_pow, ← map_mul, ← pow_add, Nat.sub_add_cancel h]
· rw [← neg_sub, ← Int.ofNat_sub (le_of_not_ge h), selfZPow_neg_natCast, IsLocalization.mk'_eq_iff_eq]
simp [Submonoid.pow_apply, ← pow_add, Nat.sub_add_cancel (le_of_not_ge h)]
