instNonemptyChooseBasisIndexOfNontrivial

Mathlib.LinearAlgebra.FreeModule.Basic

URI: https://scilib.ai/kg/mathlib#Module.Free.instNonemptyChooseBasisIndexOfNontrivial

English

If M is nontrivial, then the index type ChooseBasisIndex R M is nonempty.

Русский

Если M ненулевой, то ChooseBasisIndex R M ненулевой (непустой).

LaTeX

$$$$ [Nontrivial\ M] \Rightarrow \mathrm{Nonempty}(\mathrm{ChooseBasisIndex}(R,M)) $$$$

Lean4

instance [Nontrivial M] : Nonempty (Module.Free.ChooseBasisIndex R M) :=
  (Module.Free.chooseBasis R M).index_nonempty

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

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

Разделы

Аффилиация

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