coe_injective

Mathlib.RingTheory.Derivation.Basic

URI: https://scilib.ai/kg/mathlib#Derivation.coe_injective

English

Two derivations are equal if they have the same action on every element of A.

Русский

Две производные равны, если для каждого элемента A эти их значения совпадают.

LaTeX

$$D_1 = D_2 \Rightarrow D_1(a) = D_2(a) \quad \forall a \in A.$$

Lean4

theorem coe_injective : @Function.Injective (Derivation R A M) (A → M) DFunLike.coe :=
  DFunLike.coe_injective

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru