left

Mathlib.RingTheory.PicardGroup

URI: https://scilib.ai/kg/mathlib#Module.Invertible.left

English

From an isomorphism e: M ⊗ N ≃ R, one obtains a right-invertible structure for M.

Русский

Из изоморфизма e: M ⊗ N ≃ R следует правообратимая структура для M.

LaTeX

$$Module.Invertible.right$$

Lean4

protected theorem left : Module.Invertible R M :=
  .right (TensorProduct.comm R N M ≪≫ₗ e)

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

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

Разделы

Аффилиация

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