rank_baseChange

Mathlib.LinearAlgebra.Dimension.Constructions

URI: https://scilib.ai/kg/mathlib#Module.rank_baseChange

English

If M has rank n, there exists a linear equivalence M ≃ Fin n → R.

Русский

Если размерность M равна n, существует линейное эквивалентное отображение M ≃ Fin n → R.

LaTeX

$$$ (\\operatorname{Module.rank} R M = n) \\Rightarrow \\exists e: M \\simeq_R \\mathrm{Fin}\\,n \\to R. $$$

Lean4

theorem rank_baseChange : Module.rank R (R ⊗[S] M') = Cardinal.lift.{u} (Module.rank S M') := by simp

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

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

Разделы

Аффилиация

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