toCotangent_range

Mathlib.RingTheory.Ideal.Cotangent

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

English

The range of I.toCotangent is the entire cotangent module, i.e., range I.toCotangent = ⊤.

Русский

Образ I.toCotangent равен всем модулю котонтанта: range I.toCotangent = ⊤.

LaTeX

$$$\\mathrm{range}(I.toCotangent) = \\top$$$

Lean4

theorem toCotangent_range : LinearMap.range I.toCotangent = ⊤ :=
  Submodule.range_mkQ _

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

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

Разделы

Аффилиация

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