mk_range_eq_rank

Mathlib.LinearAlgebra.Dimension.StrongRankCondition

URI: https://scilib.ai/kg/mathlib#Module.Basis.mk_range_eq_rank

English

For a basis v: ι → M, the cardinality of the range of v equals the rank of M, i.e., |range(v)| = rank_R(M).

Русский

Для базиса v: ι → M кардинальность множества range(v) равна рангу модуля: |range(v)| = rank_R(M).

LaTeX

$$$|\\mathrm{range}(v)| = \\operatorname{rank}_R(M)$$$

Lean4

theorem mk_range_eq_rank (v : Basis ι R M) : #(range v) = Module.rank R M :=
  v.reindexRange.mk_eq_rank''

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

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

Разделы

Аффилиация

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