English
If f: E ≃ₗᵢ[ℝ] ℂ identifies E with ℂ in a way compatible with the orientation, then for all x,y ∈ E, the area form is given by ω(x,y) = Im( overline{f(x)} f(y) ).
Русский
Если f: E ≃ₗᵢ[ℝ] ℂ сопоставляет пространство E с ℂ совместно с ориентацией, то для всех x,y ∈ E форма площади удовлетворяет ω(x,y) = Im( overline{f(x)} f(y) ).
LaTeX
$$$ \\omega(x,y) = \\operatorname{Im}(\\overline{f(x)} \\; f(y)) $$$
Lean4
/-- The area form on an oriented real inner product space of dimension 2 can be evaluated in terms
of a complex-number representation of the space. -/
theorem areaForm_map_complex (f : E ≃ₗᵢ[ℝ] ℂ) (hf : Orientation.map (Fin 2) f.toLinearEquiv o = Complex.orientation)
(x y : E) : ω x y = (conj (f x) * f y).im :=
by
rw [← Complex.areaForm, ← hf, areaForm_map]
iterate 2 rw [LinearIsometryEquiv.symm_apply_apply]
