re_apply_eq_re_of_add_conj_eq — Mathlib

English

If a linear isometry f fixes 1 in the real-linear sense, then for any z, the imaginary part satisfies (f z).re = z.re and (f z).im is either z.im or - z.im, with a certain relation.

Русский

Если линейная изометрия f фиксирует 1, то для любого z выполняется (f z).re = z.re и (f z).im равно либо z.im, либо - z.im, с соответствующим соотношением.

LaTeX

$$$\forall {f : ℂ \toℓᵢ[ℝ] ℂ}, (f \;1 = 1) \rightarrow \forall z, \; (f z).im = z.im \lor (f z).im = -z.im$$$

Lean4

theorem re_apply_eq_re_of_add_conj_eq (f : ℂ →ₗᵢ[ℝ] ℂ) (h₃ : ∀ z, z + conj z = f z + conj (f z)) (z : ℂ) :
    (f z).re = z.re := by
  simpa [Complex.ext_iff, add_re, add_im, conj_re, conj_im, ← two_mul, show (2 : ℝ) ≠ 0 by simp] using (h₃ z).symm

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