Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-21 04:59 02a56964

View on Github →

feat(analysis/normed_space): Define conformal maps on inner product spaces; define the groupoid of conformal maps (#8367)

Estimated changes

added theorem conformal.comp
added theorem conformal.conformal_at
added theorem conformal.const_smul
added def conformal
added theorem conformal_at.comp
added theorem conformal_at.congr
added def conformal_at
added theorem conformal_at_id
added theorem conformal_at_iff'
added theorem conformal_at_iff
added theorem conformal_const_smul
added theorem conformal_id
added theorem is_conformal_map.comp
added def is_conformal_map
added theorem is_conformal_map_id
added theorem is_conformal_map_iff