Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-23 21:18 54eb6037

View on Github →

chore(analysis/normed_space/conformal_linear_map): delay dependence on inner products (#9293)

Estimated changes

Created src/analysis/calculus/conformal/inner_product.lean

added theorem conformal_at_iff'

added theorem conformal_at_iff

added def conformal_factor_at

added theorem conformal_factor_at_inner_eq_mul_inner'

added theorem conformal_factor_at_inner_eq_mul_inner

added theorem conformal_factor_at_pos

Renamed src/analysis/calculus/conformal.lean to src/analysis/calculus/conformal/normed_space.lean

deleted def conformal_at.conformal_factor_at

deleted theorem conformal_at.conformal_factor_at_inner_eq_mul_inner'

deleted theorem conformal_at.conformal_factor_at_inner_eq_mul_inner

deleted theorem conformal_at.conformal_factor_at_pos

deleted theorem conformal_at_iff'

deleted theorem conformal_at_iff

Modified src/analysis/complex/real_deriv.lean

Modified src/analysis/normed_space/conformal_linear_map.lean

modified theorem is_conformal_map.injective

modified theorem is_conformal_map.ne_zero

modified def is_conformal_map

deleted theorem is_conformal_map_iff

modified theorem linear_isometry.is_conformal_map

Created src/analysis/normed_space/conformal_linear_map/inner_product.lean

added theorem is_conformal_map_iff

Modified src/geometry/euclidean/basic.lean

Modified src/geometry/manifold/conformal_groupoid.lean