English
Let E be a real two–dimensional oriented inner product space. Under the standard complex-coordinate identification given by the orientation, the area form ω is given by the imaginary part of the product with the complex conjugate: ω(w,z) = Im( overline{w} z ) for all w,z ∈ C.
Русский
Пусть E — ориентированное вещественное двумерное пространство с внутренним произведением. Под стандартным комплексным представлением, заданным ориентацией, форма площади удовлетворяет ω(w,z) = Im( \overline{w} z ) для всех w,z ∈ C.
LaTeX
$$$ \\omega(w,z) = \\operatorname{Im}(\\overline{w} z) $$$
Lean4
@[simp]
protected theorem areaForm (w z : ℂ) : Complex.orientation.areaForm w z = (conj w * z).im :=
by
let o := Complex.orientation
simp only [o, o.areaForm_to_volumeForm, o.volumeForm_robust Complex.orthonormalBasisOneI rfl, Basis.det_apply,
Matrix.det_fin_two, Basis.toMatrix_apply, toBasis_orthonormalBasisOneI, Matrix.cons_val_zero, coe_basisOneI_repr,
Matrix.cons_val_one, mul_im, conj_re, conj_im]
ring
