h1Cotangentι_injective

Mathlib.RingTheory.Extension.Cotangent.Basic

URI: https://scilib.ai/kg/mathlib#Algebra.Extension.h1Cotangentι_injective

English

The construction H1Cotangent respects a scalar tower in the sense that IsScalarTower R R' S' holds for P.H1Cotangent.

Русский

Конструкция H1Cotangent сохраняет структуру вертикального каскада: IsScalarTower R R' S' выполняется для P.H1Cotangent.

LaTeX

$$IsScalarTower R R' P.H1Cotangent$$

Lean4

theorem h1Cotangentι_injective : Function.Injective P.h1Cotangentι :=
  Subtype.val_injective

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

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

Разделы

Аффилиация

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