English
Conjugate symmetry: conj ⟨y,x⟩ = ⟨x,y⟩.
Русский
Симметрия сопряжённого: conj ⟨y, x⟩ = ⟨x, y⟩.
LaTeX
$$$\overline{\langle y,x\rangle} = \langle x,y\rangle$$$
Lean4
theorem conj_symm (x y : E) : conj (inner_ 𝕜 y x) = inner_ 𝕜 x y :=
by
simp only [inner_, map_sub, map_add, map_mul, map_inv₀, map_ofNat, conj_ofReal, conj_I]
rw [add_comm y x, norm_sub_rev]
by_cases hI : (I : 𝕜) = 0
· simp only [hI, neg_zero, zero_mul]
have hI' := I_mul_I_of_nonzero hI
have I_smul (v : E) : ‖(I : 𝕜) • v‖ = ‖v‖ := by rw [norm_smul, norm_I_of_ne_zero hI, one_mul]
have h₁ : ‖(I : 𝕜) • y - x‖ = ‖(I : 𝕜) • x + y‖ :=
by
convert I_smul ((I : 𝕜) • x + y) using 2
linear_combination (norm := module) -hI' • x
have h₂ : ‖(I : 𝕜) • y + x‖ = ‖(I : 𝕜) • x - y‖ :=
by
convert (I_smul ((I : 𝕜) • y + x)).symm using 2
linear_combination (norm := module) -hI' • y
rw [h₁, h₂]
ring
