polarCoord_symm_eq

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

URI: https://scilib.ai/kg/mathlib#NumberField.mixedEmbedding.polarCoord_symm_eq

English

The targets of polarCoord and polarCoordReal coincide.

Русский

Цели polarCoord и polarCoordReal совпадают.

LaTeX

$$$(polarCoord(K)).target = (polarCoordReal(K)).target$$$

Lean4

theorem polarCoord_symm_eq :
    (mixedEmbedding.polarCoord K).symm = (mixedSpaceToRealMixedSpace K).symm ∘ (polarCoordReal K).symm :=
  rfl

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

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

Разделы

Аффилиация

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