instIsScalarTowerResidueFieldCotangentSpace

Mathlib.RingTheory.Ideal.Cotangent

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

English

There is a scalar tower R → ResidueField R → CotangentSpace R in IsLocalRing contexts.

Русский

Существует скалярная башня R → ResidueField R → CotangentSpace R в контексте IsLocalRing.

LaTeX

$$IsScalarTower R (ResidueField R) (CotangentSpace R)$$

Lean4

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

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

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

Разделы

Аффилиация

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