finBasisOfFinrankEq

Mathlib.LinearAlgebra.Dimension.Free

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

← MathLib Explorer

English

If finrank R M = n, then there is a Basis Fin n R M.

Русский

Если финразмерность равна n, существует база Fin n для M над R.

LaTeX

$$$$ \\exists b:\\ Basis(\\mathrm{Fin}(n))\\;R\\;M $$$$

Lean4

/-- A rank `n` free module has a basis indexed by `Fin n`. -/
noncomputable def finBasisOfFinrankEq [Module.Finite R M] {n : ℕ} (hn : finrank R M = n) : Basis (Fin n) R M :=
  (finBasis R M).reindex (finCongr hn)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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