submodule_invertible

Mathlib.RingTheory.PicardGroup

URI: https://scilib.ai/kg/mathlib#Units.submodule_invertible

English

If I is a unit of Submodule R A, then I is invertible as an R-module.

Русский

Если I — единичный элемент подмодуля Submodule R A, то I инвертируем как R-модуль.

LaTeX

$$$ \\forall (I : \\mathrm{Units}( \\mathrm{Submodule} R A )), \\; \\mathrm{Module.Invertible} R I. $$$

Lean4

theorem _root_.Units.submodule_invertible : Module.Invertible R I :=
  .left (tensorInvEquiv S I)

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

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

Разделы

Аффилиация

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