congr_fun

Mathlib.RingTheory.Derivation.Basic

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

English

If two derivations are equal, they have equal values on any input.

Русский

Если две производные равны, их значения на любом входе совпадают.

LaTeX

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

Lean4

theorem congr_fun (h : D1 = D2) (a : A) : D1 a = D2 a :=
  DFunLike.congr_fun h a

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

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

Разделы

Аффилиация

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