inv_eq_dual

Mathlib.RingTheory.PicardGroup

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

English

For any M in Pic(R), M⁻¹ equals Pic.mk R (Dual R M).

Русский

Для любого M в Pic(R) элемент M⁻¹ равен Pic.mk R (Dual R M).

LaTeX

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

Lean4

theorem inv_eq_dual (M : Pic R) : M⁻¹ = Pic.mk R (Dual R M) := by rw [mk_dual, mk_eq_self]

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

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

Разделы

Аффилиация

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