English
If two derivations agree on a set s, they agree on adjoin(R, s).
Русский
Если две производные совпадают на множестве s, то они совпадают на adjoin(R, s).
LaTeX
$$Set.EqOn (Derivation.instFunLike.coe D1) (Derivation.instFunLike.coe D2) s → Set.EqOn (Derivation.instFunLike.coe D1) (Derivation.instFunLike.coe D2) (Algebra.adjoin R s).$$
Lean4
@[simp]
theorem leibniz_pow (n : ℕ) : D (a ^ n) = n • a ^ (n - 1) • D a := by
induction n with
| zero => rw [pow_zero, map_one_eq_zero, zero_smul]
| succ n ihn =>
rcases (zero_le n).eq_or_lt with (rfl | hpos)
· simp
· have : a * a ^ (n - 1) = a ^ n := by rw [← pow_succ', Nat.sub_add_cancel hpos]
simp only [pow_succ', leibniz, ihn, smul_comm a n (_ : M), smul_smul a, add_smul, this, Nat.add_succ_sub_one,
add_zero, one_nsmul]
