Mathlib v3 is deprecated. Go to Mathlib v4

Theorem inner_product_geometry.conformal_at.preserves_angle

Modification history

2023-03-24 21:41
src/geometry/euclidean/angle/unoriented/conformal.lean
refactor(analysis/inner_product_space/basic): do not extend normed_add_comm_group (#18583) …
Modified inner_product_geometry.conformal_at.preserves_angleView on Github →
2023-01-18 17:47
src/geometry/euclidean/angle/unoriented/basic.lean
refactor(geometry/euclidean/angle/unoriented/basic): split out conformal map lemmas (#18210) …
Modified inner_product_geometry.conformal_at.preserves_angleView on Github →
2022-10-13 06:01
src/geometry/euclidean/angle/unoriented/basic.lean
refactor(geometry/euclidean): split up unoriented angles (#16942) …
Modified inner_product_geometry.conformal_at.preserves_angleView on Github →
2021-08-07 19:53
src/geometry/euclidean/basic.lean
feat(analysis/complex): prove that complex functions are conformal if and only if the functions are holomorphic/antiholomorphic with nonvanishing differential (#8424) …
Added inner_product_geometry.conformal_at.preserves_angleView on Github →