rank_eq_one

Mathlib.RingTheory.PicardGroup

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

English

Under the strong rank condition and freeness, the module M has rank 1 over R.

Русский

При условии сильного ранга и свободы модуль M имеет ранг 1 над R.

LaTeX

$$$\operatorname{rank}_R(M) = 1$$$

Lean4

theorem rank_eq_one [StrongRankCondition R] [Free R M] : Module.rank R M = 1 :=
  rank_eq_one_iff_finrank_eq_one.mpr (finrank_eq_one R M)

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

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

Разделы

Аффилиация

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