Cotangent

Mathlib.RingTheory.Ideal.Cotangent

URI: https://scilib.ai/kg/mathlib#Ideal.Cotangent

English

The cotangent map I.toCotangent from I to I.Cotangent is surjective for any ideal I in a ring.

Русский

Коотангенентная карта I.toCotangent отражает сюръективность.

LaTeX

$$$\\text{Surjective } I.toCotangent$$$

Lean4

/-- `I ⧸ I ^ 2` as a quotient of `I`. -/
def Cotangent : Type _ :=
  I ⧸ (I • ⊤ : Submodule R I)
deriving Inhabited, AddCommGroup, Module (R ⧸ I)

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

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

Разделы

Аффилиация

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