instTensorProduct

Mathlib.RingTheory.PicardGroup

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

← MathLib Explorer

English

Invertible modules are projective; M is projective over R.

Русский

Обратимый модуль является проектительным над R.

LaTeX

$$Module.Projective R M$$

Lean4

instance [Module.Invertible R N] : Module.Invertible R (M ⊗[R] N) :=
  .right (M := Dual R M ⊗[R] Dual R N) <|
    tensorTensorTensorComm .. ≪≫ₗ congr (linearEquiv R M) (linearEquiv R N) ≪≫ₗ TensorProduct.lid R R

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

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

Разделы

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

Аффилиация

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