Mathlib v3 is deprecated. Go to Mathlib v4

Theorem dist_div_norm_sq_smul

Modification history

2022-06-18 16:59
src/analysis/inner_product_space/basic.lean
feat(geometry/euclidean/inversion) new file (#14692) …
Added dist_div_norm_sq_smulView on Github →