conjugate_coe_eq

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

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

English

For φ: K →+* ℂ, and x ∈ K, the coefficient-level evaluation of conjugate φ equals conj(φ x).

Русский

Для φ: K →+* ℂ и x ∈ K, равенство коэффициентов выражается как conjugate φ(x) = conj(φ x).

LaTeX

$$conjugate φ x = conj (φ x)$$

Lean4

@[simp]
theorem conjugate_coe_eq (φ : K →+* ℂ) (x : K) : (conjugate φ) x = conj (φ x) :=
  rfl

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

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

Разделы

Аффилиация

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