mk_eq_one_iff

Mathlib.RingTheory.PicardGroup

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

English

For any M in Pic(R), M⁻¹ is represented by Pic.mk R (Dual R M).

Русский

Для любого M из Pic(R) обратный элемент M⁻¹ представлен как Pic.mk R (Dual R M).

LaTeX

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

Lean4

theorem mk_eq_one_iff : Pic.mk R M = 1 ↔ Nonempty (M ≃ₗ[R] R) := by rw [← mk_self, mk_eq_mk_iff]

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

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

Разделы

Аффилиация

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