pi_L2): Distance formula in the euclidean space (#14642)

Commit

3 years ago

feat(analysis/inner_product_space/pi_L2): Distance formula in the euclidean space (#14642) A few missing results about `pi_Lp 2` and `euclidean_space`.

Author

YaelDillies

Parents

ac0ce64c

mathlib3 7b4680fe - feat(analysis/inner_product_space/pi_L2): Distance formula in the euclidean space (#14642)

mathlib3
7b4680fe - feat(analysis/inner_product_space/pi_L2): Distance formula in the euclidean space (#14642)