infinite

Mathlib.LinearAlgebra.FreeModule.Basic

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

English

If R is Infinite and M is nontrivial, then M is Infinite.

Русский

Если R бесконечен и M ненулевой, то M бесконечно (неконечен).

LaTeX

$$$$ [Infinite\ R] \;[Nontrivial\ M] \Rightarrow \ Infinite\ M $$$$

Lean4

theorem infinite [Infinite R] [Nontrivial M] : Infinite M :=
  (Equiv.infinite_iff (chooseBasis R M).repr.toEquiv).mpr Finsupp.infinite_of_right

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

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

Разделы

Аффилиация

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