toComplex_star — Mathlib

English

The embedding interacts with complex conjugation via star: toComplex(star x) equals conjugate of toComplex(x).

Русский

Отображение взаимодействует со звездой: toComplex(star x) = conj(toComplex(x)).

LaTeX

$$@[simp] theorem toComplex_star (x : ℤ[i]) : ((star x : ℤ[i]) : ℂ) = conj (x : ℂ) := ...$$

Lean4

@[simp]
theorem toComplex_star (x : ℤ[i]) : ((star x : ℤ[i]) : ℂ) = conj (x : ℂ) :=
  by
  rw [toComplex_def₂, toComplex_def₂]
  exact congr_arg₂ _ rfl (Int.cast_neg _)

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