instFiniteDimensionalReal

Mathlib.LinearAlgebra.Complex.FiniteDimensional

URI: https://scilib.ai/kg/mathlib#Complex.instFiniteDimensionalReal

English

The complex field is finite-dimensional as a vector space over the real numbers.

Русский

Комплекс как векторное пространство над вещественными числами конечноразмерно.

LaTeX

$$FiniteDimensional Real Complex.$$

Lean4

instance : FiniteDimensional ℝ ℂ :=
  .of_fintype_basis basisOneI

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

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

Разделы

Аффилиация

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