English
Inverse relationship: selfZPow (−d) · selfZPow d = 1.
Русский
Обратное отношение: selfZPow (−d) · selfZPow d = 1.
LaTeX
$$$selfZPow(x,B,-d) \cdot selfZPow(x,B,d) = 1$$$
Lean4
theorem selfZPow_pow_sub (a : R) (b : B) (m d : ℤ) :
selfZPow x B (m - d) * mk' B a (1 : Submonoid.powers x) = b ↔
selfZPow x B m * mk' B a (1 : Submonoid.powers x) = selfZPow x B d * b :=
by
rw [sub_eq_add_neg, selfZPow_add, mul_assoc, mul_comm _ (mk' B a 1), ← mul_assoc]
constructor
· intro h
have := congr_arg (fun s : B => s * selfZPow x B d) h
simp only at this
rwa [mul_assoc, mul_assoc, selfZPow_neg_mul, mul_one, mul_comm b _] at this
· intro h
have := congr_arg (fun s : B => s * selfZPow x B (-d)) h
simp only at this
rwa [mul_comm _ b, mul_assoc b _ _, selfZPow_mul_neg, mul_one] at this
