instSubsingletonOfIsLocalRing

Mathlib.RingTheory.PicardGroup

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

English

If R is a local ring, then Pic(R) is subsingleton (trivial Picard group).

Русский

Если R локальное кольцо, то Pic(R) тривиальна.

LaTeX

$$$ \\text{If } R \\text{ is local}, \\; \\mathrm{Subsingleton}(\\mathrm{Pic}(R)). $$$

Lean4

instance [IsLocalRing R] : Subsingleton (Pic R) :=
  subsingleton_iff.mpr fun _ _ _ _ ↦ free_of_flat_of_isLocalRing

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

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

Разделы

Аффилиация

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