mathlib

bdcb5fb7 - feat(analysis/inner_product_space/two_dim): the case of `ℂ` (#16929)

feat(analysis/inner_product_space/two_dim): the case of `ℂ` (#16929) This file relates the constructions `orientation.area_form`, `orientation.right_angle_rotation`, `orientation.kahler` on an oriented two-dimensional real inner product space to their concrete interpretations over `ℂ`.