mk_self

Mathlib.RingTheory.PicardGroup

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

English

Pic.mk R R = 1, i.e., the Picard class of the ring R is the identity.

Русский

Pic.mk R R = 1, то есть классПикарда кольца R является тождественным элементом.

LaTeX

$$$ \\mathrm{Pic.mk} R R = 1. $$$

Lean4

theorem mk_self : Pic.mk R R = 1 :=
  congr_arg (equivShrink _) <| Units.ext <| Quotient.sound ⟨(Finite.reprEquiv R R).toModuleIso⟩

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

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

Разделы

Аффилиация

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