mk_dual

Mathlib.RingTheory.PicardGroup

URI: https://scilib.ai/kg/mathlib#CommRing.Pic.mk_dual

← MathLib Explorer

English

The inverse of M is Pic.mk R (Dual R M).

Русский

Обратный модуль M задаётся как Pic.mk R (Dual R M).

LaTeX

$$$ \\mathrm{Pic.mk} R (\\mathrm{Dual} R M) = M^{-1}. $$$

Lean4

theorem mk_dual : Pic.mk R (Dual R M) = (Pic.mk R M)⁻¹ :=
  congr_arg (equivShrink _) <|
    Units.ext <| by
      rw [Pic.mk, Equiv.symm_apply_apply]
      exact Quotient.sound ⟨(Finite.reprEquiv R _ ≪≫ₗ (Finite.reprEquiv R _).dualMap).toModuleIso⟩

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

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

Разделы

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

Аффилиация

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