mk_eq_self

Mathlib.RingTheory.PicardGroup

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

English

For any M in Pic(R), Pic.mk R M = M (as a Picard element).

Русский

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

LaTeX

$$$ \\mathrm{Pic.mk} R M = M,. $$$

Lean4

theorem mk_eq_self {M : Pic R} : Pic.mk R M = M :=
  mk_eq_iff.mpr ⟨.refl ..⟩

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

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

Разделы

Аффилиация

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