Commit 2022-10-13 20:27 a08db7e9

View on Github →

feat(analysis/inner_product_space/two_dim): new file (#16928) This file defines constructions specific to the geometry of an oriented two-dimensional real inner product space. Main declarations:

orientation.area_form
orientation.right_angle_rotation
orientation.kahler (renaming suggestions are welcome) Zulip

Estimated changes

Created src/analysis/inner_product_space/two_dim.lean

added theorem orientation.abs_area_form_le

added theorem orientation.abs_area_form_of_orthogonal

added theorem orientation.abs_kahler

added def orientation.area_form'

added theorem orientation.area_form'_apply

added def orientation.area_form

added theorem orientation.area_form_apply_self

added theorem orientation.area_form_comp_right_angle_rotation

added theorem orientation.area_form_le

added theorem orientation.area_form_right_angle_rotation_left

added theorem orientation.area_form_right_angle_rotation_right

added theorem orientation.area_form_swap

added theorem orientation.area_form_to_volume_form

added def orientation.basis_right_angle_rotation

added theorem orientation.coe_basis_right_angle_rotation

added theorem orientation.eq_zero_or_eq_zero_of_kahler_eq_zero

added theorem orientation.inner_comp_right_angle_rotation

added theorem orientation.inner_mul_area_form_sub'

added theorem orientation.inner_mul_area_form_sub

added theorem orientation.inner_mul_inner_add_area_form_mul_area_form'

added theorem orientation.inner_mul_inner_add_area_form_mul_area_form

added theorem orientation.inner_right_angle_rotation_aux₁_left

added theorem orientation.inner_right_angle_rotation_aux₁_right

added theorem orientation.inner_right_angle_rotation_left

added theorem orientation.inner_right_angle_rotation_right

added theorem orientation.inner_right_angle_rotation_self

added theorem orientation.inner_right_angle_rotation_swap'

added theorem orientation.inner_right_angle_rotation_swap

added theorem orientation.inner_sq_add_area_form_sq

added def orientation.kahler

added theorem orientation.kahler_apply_apply

added theorem orientation.kahler_apply_self

added theorem orientation.kahler_comp_right_angle_rotation

added theorem orientation.kahler_eq_zero_iff

added theorem orientation.kahler_mul

added theorem orientation.kahler_ne_zero

added theorem orientation.kahler_ne_zero_iff

added theorem orientation.kahler_right_angle_rotation_left

added theorem orientation.kahler_right_angle_rotation_right

added theorem orientation.kahler_swap

added theorem orientation.nonneg_inner_and_area_form_eq_zero_iff_same_ray

added theorem orientation.norm_kahler

added theorem orientation.norm_sq_kahler

added def orientation.right_angle_rotation

added def orientation.right_angle_rotation_aux₁

added theorem orientation.right_angle_rotation_aux₁_right_angle_rotation_aux₁

added def orientation.right_angle_rotation_aux₂

added theorem orientation.right_angle_rotation_right_angle_rotation

added theorem orientation.right_angle_rotation_symm

added theorem orientation.right_angle_rotation_trans_right_angle_rotation

Modified src/analysis/normed_space/linear_isometry.lean

added theorem linear_isometry_equiv.coe_of_linear_isometry

added theorem linear_isometry_equiv.coe_of_linear_isometry_symm

added def linear_isometry_equiv.of_linear_isometry