English
There is a canonical negation operation on Derivation making it into an additive group.
Русский
Существует каноническое отрицание выводов, образующее добавочную группу.
LaTeX
$$Derivation R A M forms a group under addition with negation defined by mk'(-D, …).$$
Lean4
theorem leibniz_zpow (a : K) (n : ℤ) : D (a ^ n) = n • a ^ (n - 1) • D a :=
by
by_cases hn : n = 0
· simp [hn]
by_cases ha : a = 0
· simp [ha, zero_zpow n hn]
rcases Int.natAbs_eq n with h | h
· rw [h]
simp only [zpow_natCast, leibniz_pow, natCast_zsmul]
rw [← zpow_natCast]
congr
cutsat
· rw [h, zpow_neg, zpow_natCast, leibniz_inv, leibniz_pow, inv_pow, ← pow_mul, ← zpow_natCast, ← zpow_natCast, ←
Nat.cast_smul_eq_nsmul K, ← Int.cast_smul_eq_zsmul K, smul_smul, smul_smul, smul_smul]
trans (-n.natAbs * (a ^ ((n.natAbs - 1 : ℕ) : ℤ) / (a ^ ((n.natAbs * 2 : ℕ) : ℤ)))) • D a
· ring_nf
rw [← zpow_sub₀ ha]
congr 3
· norm_cast
cutsat
