Mathlib v3 is deprecated. Go to Mathlib v4

Theorem conformal_at.const_smul

Modification history

2021-07-21 04:59

src/analysis/calculus/conformal.lean

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

Added conformal_at.const_smul View on Github →