trans

Mathlib.LinearAlgebra.FiniteDimensional.Defs

URI: https://scilib.ai/kg/mathlib#FiniteDimensional.trans

English

If F/K and K/A are finite-dimensional, then F/A is finite-dimensional.

Русский

Если F над K конечномерно, а K над A конечномерно, то F над A конечномерно.

LaTeX

$$FiniteDimensional F K ∧ FiniteDimensional K A ⇒ FiniteDimensional F A$$

Lean4

theorem trans [FiniteDimensional F K] [FiniteDimensional K A] : FiniteDimensional F A :=
  Module.Finite.trans K A

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

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

Разделы

Аффилиация

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