instModuleCotangent

Mathlib.RingTheory.Extension.Basic

URI: https://scilib.ai/kg/mathlib#Algebra.Extension.instModuleCotangent

English

The action of an element r from R on x in P.Cotangent satisfies (r • x).val = r • x.val.

Русский

Действие элемента r из R на x в P.Cotangent удовлетворяет (r • x).val = r • x.val.

LaTeX

$$$$ (r \cdot x).val = r \cdot x.val \quad (r \in R, x \in P.Cotangent) $$$$

Lean4

noncomputable instance {R₀} [CommRing R₀] [Algebra R₀ S] : Module R₀ P.Cotangent :=
  Module.compHom P.Cotangent (algebraMap R₀ S)

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

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

Разделы

Аффилиация

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