instModuleResidueFieldCotangentSpace

Mathlib.RingTheory.Ideal.Cotangent

URI: https://scilib.ai/kg/mathlib#IsLocalRing.instModuleResidueFieldCotangentSpace

English

There is a module structure of the residue field on the cotangent space of a local ring.

Русский

Существует модульная структура остаточного поля над котантентной пространством локального кольца.

LaTeX

$$Module (ResidueField R) (CotangentSpace R)$$

Lean4

instance : Module (ResidueField R) (CotangentSpace R) :=
  inferInstanceAs <| Module (R ⧸ maximalIdeal R) _

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

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

Разделы

Аффилиация

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