Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-20 07:06 bdcb5fb7

View on Github →

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 ℂ.

Estimated changes

Modified src/analysis/inner_product_space/basic.lean

added theorem inner_map_complex

Modified src/analysis/inner_product_space/orientation.lean

added theorem orientation.volume_form_comp_linear_isometry_equiv

added theorem orientation.volume_form_map

Modified src/analysis/inner_product_space/two_dim.lean

added theorem orientation.area_form_comp_linear_isometry_equiv

added theorem orientation.area_form_map

added theorem orientation.area_form_map_complex

added theorem orientation.kahler_comp_linear_isometry_equiv

added theorem orientation.kahler_map

added theorem orientation.kahler_map_complex

added theorem orientation.linear_isometry_equiv_comp_right_angle_rotation'

added theorem orientation.linear_isometry_equiv_comp_right_angle_rotation

added theorem orientation.right_angle_rotation_map'

added theorem orientation.right_angle_rotation_map

added theorem orientation.right_angle_rotation_map_complex

Modified src/data/complex/module.lean

Modified src/linear_algebra/determinant.lean

added theorem linear_map.det_eq_one_of_finrank_eq_zero

added theorem linear_map.det_eq_one_of_subsingleton

Modified src/linear_algebra/orientation.lean

added theorem orientation.map_of_is_empty

added theorem orientation.map_positive_orientation_of_is_empty

Modified src/linear_algebra/ray.lean