fintype

Mathlib.LinearAlgebra.Quotient.Basic

URI: https://scilib.ai/kg/mathlib#Submodule.QuotientTop.fintype

English

If M is finite, then the quotient M / ⊤ is finite (in particular, it is a finite type).

Русский

Если M конечно, то фактор-модуль M / ⊤ конечно, то есть имеет конечную размерность/тип.

LaTeX

$$$$ \\text{If } M \\text{ is finite, then } M / \\top \\text{ is finite}. $$$$

Lean4

instance fintype : Fintype (M ⧸ (⊤ : Submodule R M)) :=
  Fintype.ofSubsingleton 0

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

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

Разделы

Аффилиация

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