Mathlib v3 is deprecated. Go to Mathlib v4

Def conformal_factor_at

Modification history

2021-09-23 21:18

src/analysis/calculus/conformal/inner_product.lean

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

Added conformal_factor_at View on Github →