rank_punit

Mathlib.LinearAlgebra.Dimension.Subsingleton

URI: https://scilib.ai/kg/mathlib#rank_punit

English

The rank of the one-point type PUnit is zero: rank_R PUnit = 0.

Русский

Ранк типа PUnit равен нулю: rank_R PUnit = 0.

LaTeX

$$$\\operatorname{Module.rank} R \\; \\mathbf{PUnit} = 0$$$

Lean4

theorem rank_punit : Module.rank R PUnit = 0 :=
  rank_subsingleton' _ _

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

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

Разделы

Аффилиация

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