Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-08 06:14 0c424e95

View on Github →

refactor(analysis/normed_space/conformal_linear_map): redefine (#13143) Use equality of bundled maps instead of coercions to functions in the definition of is_conformal_map. Also golf some proofs.

Estimated changes

Modified src/analysis/calculus/conformal/normed_space.lean

added theorem subsingleton.conformal_at

Modified src/analysis/complex/conformal.lean

modified theorem is_conformal_map_complex_linear

Modified src/analysis/complex/real_deriv.lean

modified theorem differentiable_at.conformal_at

Modified src/analysis/inner_product_space/conformal_linear_map.lean

modified theorem is_conformal_map_iff

Modified src/analysis/normed_space/conformal_linear_map.lean

modified theorem is_conformal_map.comp

deleted theorem is_conformal_map.injective

added theorem is_conformal_map.smul

modified theorem is_conformal_map_const_smul

modified theorem is_conformal_map_of_subsingleton

deleted theorem linear_isometry.is_conformal_map

Modified src/analysis/normed_space/linear_isometry.lean

added theorem linear_isometry.coe_mk

added theorem linear_isometry.id_to_continuous_linear_map