fintype

Mathlib.LinearAlgebra.Quotient.Basic

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

English

If M is finite, then the quotient M / S is finite for any submodule S.

Русский

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

LaTeX

$$$$ \\text{If } M \\text{ is finite, then } M / S \\text{ is finite for every submodule } S. $$$$

Lean4

noncomputable instance fintype [Fintype M] (S : Submodule R M) : Fintype (M ⧸ S) :=
  @_root_.Quotient.fintype _ _ _ fun _ _ => Classical.dec _

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

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

Разделы

Аффилиация

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