apply_aeval_eq — Mathlib

English

The commutator bracket commutes with the coe to endomorphisms: the coe of bracket equals the bracket of the coe's.

Русский

Скобка коммутатора совместима с отображением в линейные отображения: коe скобки соответствует скобке коe.

LaTeX

$$$\uparrow⁅D_1,D_2⁆ = ⁅(D_1 : \mathrm{End}_R(A)), (D_2 : \mathrm{End}_R(A))⁆$$$

Lean4

theorem apply_aeval_eq [IsScalarTower R A B] [IsScalarTower A B M'] (d : Derivation R B M') (x : B) (p : A[X]) :
    d (aeval x p) = PolynomialModule.eval x ((d.compAlgebraMap A).mapCoeffs p) + aeval x (derivative p) • d x :=
  by
  convert apply_aeval_eq' (d.compAlgebraMap A) d LinearMap.id _ x p
  · apply Finsupp.ext
    intro x
    rfl
  · intro a
    rfl

Похожие утверждения