instTietzeExtension

Mathlib.Analysis.Complex.Tietze

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

English

The complex field inherits a canonical Tietze extension structure from its underlying real structure.

Русский

Комплексное поле наследует каноническую структуру расширения Титце из своей вещественной основы.

LaTeX

$$TietzeExtension ℂ$$

Lean4

instance instTietzeExtension : TietzeExtension ℂ :=
  TietzeExtension.of_tvs ℝ

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

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

Разделы

Аффилиация

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