conjCLE

Mathlib.Analysis.RCLike.Basic

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

English

Conjugation is a continuous linear equivalence over ℝ from K to K.

Русский

Сопряжение является непрерывной линейной эквивалентной отображением от K в K.

LaTeX

$$$$ conjCLE : K \\equiv^{\\text{L}[\\mathbb{R}]}_{\\mathbb{R}} K. $$$$

Lean4

/-- Conjugate as a continuous linear equivalence -/
noncomputable def conjCLE : K ≃L[ℝ] K :=
  @conjLIE K _

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

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

Разделы

Аффилиация

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