basisCotangent

Mathlib.RingTheory.Smooth.StandardSmoothCotangent

URI: https://scilib.ai/kg/mathlib#Algebra.SubmersivePresentation.basisCotangent

← MathLib Explorer

English

The classes of the relations P.relation i form a basis of I / I^2.

Русский

Классы отношений P.relation i образуют базис пространства I / I^2.

LaTeX

$$The classes of $P.relation i$ form a basis of $I / I^2$.$$

Lean4

/-- The classes of `P.relation i` form a basis of `I ⧸ I ^ 2`. -/
@[stacks 00T7 "(3)"]
noncomputable def basisCotangent : Basis σ S P.toExtension.Cotangent :=
  P.basisDeriv.map P.cotangentEquiv.symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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