conjugate

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

URI: https://scilib.ai/kg/mathlib#NumberField.ComplexEmbedding.conjugate

English

The conjugate of a complex embedding φ is a ring homomorphism conjugate φ: K →+* ℂ.

Русский

Сопряжение вложения φ - это отображение conjugate φ: K →+* ℂ.

LaTeX

$$conjugate (φ) := star φ$$

Lean4

/-- The conjugate of a complex embedding as a complex embedding. -/
abbrev conjugate (φ : K →+* ℂ) : K →+* ℂ :=
  star φ

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

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

Разделы

Аффилиация

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