restrictScalars_apply — Mathlib

English

Applying restricting scalars to a derivation yields the same underlying function as the original derivation.

Русский

Применение ограничения скаляров к деривации даёт ту же базовую функцию, что и исходная деривация.

LaTeX

$$$d.restrictScalars(R)(x) = d(x) \;\text{for all } x \in A$$$

Lean4

@[simp]
theorem restrictScalars_apply (d : Derivation S A M) (x : A) : d.restrictScalars R x = d x :=
  rfl

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