Commit 2021-08-07 19:53 d7579961

View on Github →

feat(analysis/complex): prove that complex functions are conformal if and only if the functions are holomorphic/antiholomorphic with nonvanishing differential (#8424) Complex functions are conformal if and only if the functions are holomorphic/antiholomorphic with nonvanishing differential.

Estimated changes

Modified src/analysis/calculus/conformal.lean

deleted theorem conformal_at.preserves_angle

Created src/analysis/complex/conformal.lean

added theorem is_conformal_map.is_complex_or_conj_linear

added theorem is_conformal_map_complex_linear

added theorem is_conformal_map_complex_linear_conj

added theorem is_conformal_map_conj

added theorem is_conformal_map_iff_is_complex_or_conj_linear:

Modified src/analysis/complex/real_deriv.lean

added theorem conformal_at_iff_differentiable_at_or_differentiable_at_comp_conj

added theorem differentiable_at.conformal_at

Modified src/analysis/normed_space/conformal_linear_map.lean

added theorem is_conformal_map.ne_zero

deleted theorem is_conformal_map.preserves_angle

added theorem linear_isometry.is_conformal_map

Modified src/geometry/euclidean/basic.lean

added theorem inner_product_geometry.conformal_at.preserves_angle

added theorem inner_product_geometry.is_conformal_map.preserves_angle