English
⟨x+y,z⟩ = ⟨x,z⟩ + ⟨y,z⟩.
Русский
Левая линейность: ⟨x+y,z⟩ = ⟨x,z⟩ + ⟨y,z⟩.
LaTeX
$$$\langle x+y,z\rangle = \langle x,z\rangle + \langle y,z\rangle$$$
Lean4
theorem add_left (x y z : E) : inner_ 𝕜 (x + y) z = inner_ 𝕜 x z + inner_ 𝕜 y z :=
by
unfold inner_
have h1 := parallelogram_identity (x + y + z) (x - z)
have h2 := parallelogram_identity (x + y - z) (x + z)
have h3 := parallelogram_identity (y + z) z
have h4 := parallelogram_identity (y - z) z
have h5 := parallelogram_identity ((I : 𝕜) • (x + y) + z) ((I : 𝕜) • x - z)
have h6 := parallelogram_identity ((I : 𝕜) • (x + y) - z) ((I : 𝕜) • x + z)
have h7 := parallelogram_identity ((I : 𝕜) • y + z) z
have h8 := parallelogram_identity ((I : 𝕜) • y - z) z
apply_fun 𝓚 at h1 h2 h3 h4 h5 h6 h7 h8
simp only [map_add, map_mul, map_ofNat, smul_add] at *
abel_nf at * -- TODO this should be `module_nf` (then the `smul_add` above can go)
linear_combination (-h1 + h2 + h3 - h4 + I * (-h5 + h6 + h7 - h8)) / 8
