English
The derivations form a Lie algebra under the bracket defined earlier, compatible with the A-module structure and the End(A) action.
Русский
Производные образуют алгебру Ли под скобкой, определённой ранее, совместимую с модульной структурой над A и действием End(A).
LaTeX
$$$\text{Derivation}_R(A,A) \text{ is a Lie algebra with bracket } [D_1,D_2](a)=D_1(D_2(a))-D_2(D_1(a)).$$$
Lean4
theorem apply_aeval_eq' (d' : Derivation R B M') (f : M →ₗ[A] M') (h : ∀ a, f (d a) = d' (algebraMap A B a)) (x : B)
(p : A[X]) :
d' (aeval x p) =
PolynomialModule.eval x (PolynomialModule.map B f (d.mapCoeffs p)) + aeval x (derivative p) • d' x :=
by
induction p using Polynomial.induction_on' with
| add => simp_all only [map_add, add_smul]; abel
|
monomial =>
simp only [aeval_monomial, leibniz, leibniz_pow, mapCoeffs_monomial, PolynomialModule.map_single,
PolynomialModule.eval_single, derivative_monomial, map_mul, _root_.map_natCast, h]
rw [add_comm, ← smul_smul, ← smul_smul, Nat.cast_smul_eq_nsmul]
