Mathlib Changelog
v3
Changelog
About
Github
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