Commit 2023-06-13 06:31 c285cf74

View on Github →

feat: port Analysis.InnerProductSpace.TwoDim (#4602)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/InnerProductSpace/TwoDim.lean

added theorem FiniteDimensional.finiteDimensional_of_fact_finrank_eq_two

added theorem Orientation.abs_areaForm_le

added theorem Orientation.abs_areaForm_of_orthogonal

added theorem Orientation.abs_kahler

added def Orientation.areaForm'

added theorem Orientation.areaForm'_apply

added theorem Orientation.areaForm_apply_self

added theorem Orientation.areaForm_comp_linearIsometryEquiv

added theorem Orientation.areaForm_comp_rightAngleRotation

added theorem Orientation.areaForm_le

added theorem Orientation.areaForm_map

added theorem Orientation.areaForm_map_complex

added theorem Orientation.areaForm_neg_orientation

added theorem Orientation.areaForm_rightAngleRotation_left

added theorem Orientation.areaForm_rightAngleRotation_right

added theorem Orientation.areaForm_swap

added theorem Orientation.areaForm_to_volumeForm

added def Orientation.basisRightAngleRotation

added theorem Orientation.coe_basisRightAngleRotation

added theorem Orientation.eq_zero_or_eq_zero_of_kahler_eq_zero

added theorem Orientation.inner_comp_rightAngleRotation

added theorem Orientation.inner_mul_areaForm_sub'

added theorem Orientation.inner_mul_areaForm_sub

added theorem Orientation.inner_mul_inner_add_areaForm_mul_areaForm'

added theorem Orientation.inner_mul_inner_add_areaForm_mul_areaForm

added theorem Orientation.inner_rightAngleRotationAux₁_left

added theorem Orientation.inner_rightAngleRotationAux₁_right

added theorem Orientation.inner_rightAngleRotation_left

added theorem Orientation.inner_rightAngleRotation_right

added theorem Orientation.inner_rightAngleRotation_self

added theorem Orientation.inner_rightAngleRotation_swap'

added theorem Orientation.inner_rightAngleRotation_swap

added theorem Orientation.inner_sq_add_areaForm_sq

added def Orientation.kahler

added theorem Orientation.kahler_apply_apply

added theorem Orientation.kahler_apply_self

added theorem Orientation.kahler_comp_linearIsometryEquiv

added theorem Orientation.kahler_comp_rightAngleRotation'

added theorem Orientation.kahler_comp_rightAngleRotation

added theorem Orientation.kahler_eq_zero_iff

added theorem Orientation.kahler_map

added theorem Orientation.kahler_map_complex

added theorem Orientation.kahler_mul

added theorem Orientation.kahler_ne_zero

added theorem Orientation.kahler_ne_zero_iff

added theorem Orientation.kahler_neg_orientation

added theorem Orientation.kahler_rightAngleRotation_left

added theorem Orientation.kahler_rightAngleRotation_right

added theorem Orientation.kahler_swap

added theorem Orientation.linearIsometryEquiv_comp_rightAngleRotation'

added theorem Orientation.linearIsometryEquiv_comp_rightAngleRotation

added theorem Orientation.nonneg_inner_and_areaForm_eq_zero_iff_sameRay

added theorem Orientation.normSq_kahler

added theorem Orientation.norm_kahler

added theorem Orientation.rightAngleRotationAux₁_rightAngleRotationAux₁

added def Orientation.rightAngleRotationAux₂

added theorem Orientation.rightAngleRotation_map'

added theorem Orientation.rightAngleRotation_map

added theorem Orientation.rightAngleRotation_map_complex

added theorem Orientation.rightAngleRotation_neg_orientation

added theorem Orientation.rightAngleRotation_rightAngleRotation

added theorem Orientation.rightAngleRotation_symm

added theorem Orientation.rightAngleRotation_trans_neg_orientation

added theorem Orientation.rightAngleRotation_trans_rightAngleRotation