instFinite

Mathlib.RingTheory.PicardGroup

URI: https://scilib.ai/kg/mathlib#Module.Invertible.instFinite

English

Invertible M implies M is finite; same as 182264 but listed as separate instance.

Русский

Обратимый M значит, что M конечнопроективен; повторение 182264.

LaTeX

$$Module.Finite R M$$

Lean4

instance : Module.Finite R M :=
  (finite_projective R M).1

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

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

Разделы

Аффилиация

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