coe_restrictScalars

Mathlib.RingTheory.Derivation.Basic

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

English

Restricting scalars commutes with the coe function on derivations: the underlying function remains unchanged.

Русский

Уменьшение скалярности коммутирует с приводением коe: функция деривации не меняется.

LaTeX

$$$\uparrow (d.restrictScalars R) = \uparrow d$$$

Lean4

theorem coe_restrictScalars (d : Derivation S A M) : ⇑(d.restrictScalars R) = ⇑d :=
  rfl

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

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

Разделы

Аффилиация

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