instTietzeExtension

Mathlib.Analysis.Complex.Tietze

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

English

Any RCLike field 𝕜 inherits a canonical Tietze extension structure in the same spirit as ℂ.

Русский

Любое поле RCLike 𝕜 наследует каноническую структуру расширения Титце по тому же принципу, что и ℂ.

LaTeX

$$TietzeExtension 𝕜$$

Lean4

instance (priority := 900) instTietzeExtension {𝕜 : Type*} [RCLike 𝕜] : TietzeExtension 𝕜 :=
  TietzeExtension.of_tvs ℝ

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

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

Разделы

Аффилиация

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